Как фьючерсы описываются в терминах теории категорий?

Ответы:

25

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

По сути, идея будущего заключается в том, что это структура данных, представляющая выполняемое вычисление, которое можно синхронизировать. С точки зрения временной логики, это в конечном счете , оператор . Это имеет монадическое структуру: г е т у т п : б я н д : ( B ) В , в которой г е т у т пA

return:AAbind:(AB)AB
returnОперация порождает процесс, который немедленно возвращает свой аргумент, и создает новый процесс, который ожидает значение a , применяет f к этому значению, а затем ожидает B- значения перед возвратом. Promises / Предложение по CommonJS вызывает монадическую операцию связывания , и Scala 2,10 просто дает ему стандартное монадическое интерфейс .bindafBthen

Двойственный к оператору в конечном счете является всегда оператором временной логики, в котором говорится , что в каждый момент времени , вы получите A . Когда вы переходите от семантики временной логики Крипке (где вы просто моделируете доказуемость) к категориальной семантике λ- вычисления (где вы также моделируете лямбда-термины / доказательства), оказывается, что на самом деле существует несколько способов сделать это.AAAλ

AAAA

Самое естественное (IMO), что нужно сделать, это взять , что позволяет вам получать (потенциально разные) в каждый момент времени. Затем вы можете увидеть комонадный стиль функционально-реактивного программирования (FRP) (впервые предложенный Тармо Уусталу и Вармо Вене ) как дуальный к монадическому стилю программирования с фьючерсами.AAStreamAA

Тем не менее, comonadic -calculus, как они предлагают, несмотря на его элегантность, вызывает серьезную потерю выразительности по сравнению с программированием явно с потоками, поскольку оказывается, что в категории свободных угольных алгебр, которые они используют, слишком мало глобальных элементов, чтобы обозначить много интересных программ. Особенно фиксированные точки.λ

Ник Бентон и я выступали за программирование явным образом с помощью потоков в нашей статье « Ультраметрическая семантика реактивных программ» . Впоследствии Алан Джеффри предложил использовать LTL в качестве системы типов в своей статье LTL типов FRP , наблюдение, которое Вольфганг Йельч также сделал в своей статье « К общей категориальной семантике для линейной временной темпоральной логики и функционально-реактивного программирования» .

Различие между точкой зрения, которую придерживаются Ник и я, и точкой зрения, которую придерживаются Алан и Вольфганг, лучше всего понять (IMO), если сравнить конструкцию, приведенную в «Биркедале и др.« Первые шаги в теории синтетической защищенной области: пошаговое индексирование в топосе ». деревьев с бумагой Алана. Топос деревьев (предварительные пучки над натуральными числами, упорядоченными по размеру) очень похож на категорию ультраметрических пространств, которые использовали Ник и я, но намного проще сравнить с категорией Алана (предварительные пучки над дискретной категорией времени), поскольку оба они являются предварительными пучками категории.

Если вы интересуетесь фьючерсами специально для параллелизма, то, возможно, было бы лучше взглянуть на CTL, а не на LTL. AFAIK, это в настоящее время неизведанная территория!

РЕДАКТИРОВАТЬ: вот ссылка на проект . В основном речь идет о реализации типизированного FRP, поэтому язык является синхронным. Но большая часть обсуждения фьючерсов / событий в разделе 3.3 должна в основном относиться и к действительно параллельным языкам.

Нил Кришнасвами
источник
1
Я хотел бы получить копию этого, когда вы закончите.
Дэйв Кларк
1
Кажется, что это теряет важную характеристику фьючерсов: как только значение получено, оно не может измениться. Я бы попытался выразить это, взяв в качестве аксиомы, но это не то, что мы хотим, если означает поток ... И я бы также хотел получить копию статьи, когда это будет сделано: )AA
Алексей Романов
Я недавно читал, что тип Scala Try[T]и Future[T]двойственный, но я не совсем понял, что это значит / в каком смысле.
Джорджио