Есть ли полезное описание будущего или обещания с точки зрения теории категорий? В частности, каким может быть категорический дуал будущего?
источник
Есть ли полезное описание будущего или обещания с точки зрения теории категорий? В частности, каким может быть категорический дуал будущего?
Как это происходит, я пишу статью об этом сейчас. ИМО, хороший способ думать о будущем или обещаниях с точки зрения соответствия Карри-Ховарда для временной логики .
По сути, идея будущего заключается в том, что это структура данных, представляющая выполняемое вычисление, которое можно синхронизировать. С точки зрения временной логики, это в конечном счете , оператор . Это имеет монадическое структуру: г е т у т п : → ◊ б я н д : ( → ◊ B ) → ◊ → ◊ В , в которой г е т у т п
then
Двойственный к оператору в конечном счете является всегда оператором ◻ временной логики, в котором говорится , что в каждый момент времени , вы получите A . Когда вы переходите от семантики временной логики Крипке (где вы просто моделируете доказуемость) к категориальной семантике λ- вычисления (где вы также моделируете лямбда-термины / доказательства), оказывается, что на самом деле существует несколько способов сделать это.
A
Самое естественное (IMO), что нужно сделать, это взять , что позволяет вам получать (потенциально разные) в каждый момент времени. Затем вы можете увидеть комонадный стиль функционально-реактивного программирования (FRP) (впервые предложенный Тармо Уусталу и Вармо Вене ) как дуальный к монадическому стилю программирования с фьючерсами.A
Тем не менее, comonadic -calculus, как они предлагают, несмотря на его элегантность, вызывает серьезную потерю выразительности по сравнению с программированием явно с потоками, поскольку оказывается, что в категории свободных угольных алгебр, которые они используют, слишком мало глобальных элементов, чтобы обозначить много интересных программ. Особенно фиксированные точки.
Ник Бентон и я выступали за программирование явным образом с помощью потоков в нашей статье « Ультраметрическая семантика реактивных программ» . Впоследствии Алан Джеффри предложил использовать LTL в качестве системы типов в своей статье LTL типов FRP , наблюдение, которое Вольфганг Йельч также сделал в своей статье « К общей категориальной семантике для линейной временной темпоральной логики и функционально-реактивного программирования» .
Различие между точкой зрения, которую придерживаются Ник и я, и точкой зрения, которую придерживаются Алан и Вольфганг, лучше всего понять (IMO), если сравнить конструкцию, приведенную в «Биркедале и др.« Первые шаги в теории синтетической защищенной области: пошаговое индексирование в топосе ». деревьев с бумагой Алана. Топос деревьев (предварительные пучки над натуральными числами, упорядоченными по размеру) очень похож на категорию ультраметрических пространств, которые использовали Ник и я, но намного проще сравнить с категорией Алана (предварительные пучки над дискретной категорией времени), поскольку оба они являются предварительными пучками категории.
Если вы интересуетесь фьючерсами специально для параллелизма, то, возможно, было бы лучше взглянуть на CTL, а не на LTL. AFAIK, это в настоящее время неизведанная территория!
РЕДАКТИРОВАТЬ: вот ссылка на проект . В основном речь идет о реализации типизированного FRP, поэтому язык является синхронным. Но большая часть обсуждения фьючерсов / событий в разделе 3.3 должна в основном относиться и к действительно параллельным языкам.
Try[T]
иFuture[T]
двойственный, но я не совсем понял, что это значит / в каком смысле.