Использование типов уникальности для реализации безопасного параллелизма

19

В течение некоторого времени меня интересовали типы уникальности как альтернативы монадам на чисто функциональных языках; К сожалению, это своего рода эзотерическая область исследований CS, и он-лайн ресурсы о программировании с уникальными типами очень редки.

Совершенно очевидно, как типы уникальности могут использоваться для реализации структур данных с состоянием, таких как ссылки («ящики») и массивы, хотя мне не избежать того, как вы могли бы реализовать с ними другие общие структуры данных с состоянием.

Можно ли реализовать, например, блокировку с уникальными типами? Можно ли использовать типы уникальности для совместного использования изменяемых данных между потоками? Можно ли использовать уникальные типы для создания примитивов синхронизации (например, мьютексов) или необходима передача сообщений?

Рики Стюарт
источник
Можете ли вы сделать свой вопрос немного более конкретным? Что, например, вы уже знаете о блокировке с уникальными типами и где ваших собственных знаний недостаточно?
Роберт Харви
> Что, например, вы уже знаете о блокировке с уникальными типами? Я ничего не знаю о блокировке с уникальными типами - я действительно не знаю, как работает безопасный параллелизм с уникальными типами, и я хотел бы знать, есть ли Есть какие-либо ресурсы по теме.
Рики Стюарт,
2
@RickyStewart: Вы, наверное, уже знаете Clean ( wiki.clean.cs.ru.nl/Clean ). Я просто хотел добавить ссылку, потому что вы не упомянули об этом.
Джорджио
Я думаю, что вы должны смотреть на линейные типы для параллелизма. Типы уникальности IIRC построены на линейных типах. У Фрэнка Пфеннинга есть кое-что интересное на эту тему
Даниэль Гратцер,

Ответы:

2

Можно ли реализовать, например, блокировку с уникальными типами?

Я перешел по ссылке, предоставленной Робертом Харви, и быстро прочитал. Я не могу сказать, что я все понял или что у меня высокий уровень уверенности в том, что я действительно понял то, что, как мне кажется, я понял, но мне кажется, что весь смысл внешней уникальности и эталонной неизменности заключается в том, что нет необходимости в блокировке.

Современные подходы к многопоточности стараются избегать блокировок, потому что только опытные программисты могут писать код, использующий блокировку, и даже их код подвержен ошибкам. Если вы добавите к этому тот факт, что блокировка кода практически не тестируется, должно быть очевидно, что это крайне нежелательный способ действий, и любое решение, направленное на то, чтобы освободить нас от блокировки, обещает, по меньшей мере.

Мы избегали блокировок с помощью передачи сообщений, которая требует, чтобы сообщения были неизменными. Грубо говоря, (на первый взгляд) эталонная неизменность, по-видимому, является техникой, которая может помочь нам гарантировать неизменность без фактического конструирования неизменяемых типов, а внешняя уникальность, по-видимому, является техникой, которая может помочь нам ослабить требование строгой неизменности локально.

Можно ли использовать типы уникальности для совместного использования изменяемых данных между потоками?

В документе не было четко указано, но, насколько я понимаю, внешне уникальный кластер объектов является поточно-ориентированным, потому что каким-то образом (действительно, как? ) Гарантируется, что существует только одна внешняя ссылка на этот кластер объектов, что означает, что поток, получающий такую ​​ссылку, может обрабатывать ссылочные объекты как изменяемые, не беспокоясь о том, что какой-то другой поток также может их мутировать, потому что никакой другой поток не может иметь другую ссылку. Мне было бы интересно узнать, как такая теоретическая конструкция может быть реализована и применена.

Можно ли использовать уникальные типы для создания примитивов синхронизации (например, мьютексов) или необходима передача сообщений?

Опять же, насколько я понимаю, внешне уникальные типы и ссылочная неизменность предназначены для того, чтобы сделать ненужными блокировки, мьютексы и тому подобное. Похоже, что передача сообщений - это путь, и это хорошо.

Майк Накис
источник