Okmij

Oct. 25th, 2016 07:47 am
akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Вчера у меня наконец дошли руки посмотреть на статью Freeer monads Олега Киселёва et al., и реализацию — библиотеку Eff для хаскеля. Вот блин, а. Это же надо так уметь. Шедевр, тончайшая работа.

На чистом хаскеле безо всяких макросов превратили его фактически в язык с модулярными алгебраическим эффектами. Описываешь свой эффект как в языках с алгебраическим эффектами через параметризованный GADT, т.е. просто пишешь какие ты хочешь добавить в ambient language команды с описанием их сигнатуры, пишешь ему модулярный интерпретатор, а дальше можно это свободно перемежать с другими описанными в такой же форме эффектами, умная бубиотика определяет параметрическую монаду Eff '[list of effects], всё настолько круто, что там не только композиция эффектов работает сама и полиморфные по эффектам процыдурки сами получаются, но даже effect inference для do-нотации в какой-то мере работает. И семантически очень красиво выходит: алгебраическое описание эффекта это индуктивный тип * -> *, для него конструируется левое расширение Кана, а на получившемся функторе задаётся свободная монада, вложение индуктивных типов превращается во вложение монад, соответственно “описания эффектов” можно комбинировать через disjoint sums, прощайте монадные трансформеры. В библиотеке описаны стандартные эффекты — IO, State, Non-Determinism, и всё что можно описать через Delimited Continuations (эксепшены, кооперативный мультитрединг/сопроцедуры и т.д.).

Заодно понятно, каким образом будет выглядеть комбинирование эффектов с зависимыми типами. Кажется, там ничего не сломается, кроме того что Eff станет вообще говоря относительной монадой (“монадоподобный объект, не являющийся эндофунктором”). Единственное, что мне пока не понятно — это как в сигнатуре эффекта указывать соотношения (например требовать, чтобы вызовы ReadEnv коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).

Date: 2016-10-25 06:02 am (UTC)
From: [identity profile] juan-gandhi.livejournal.com
Я никогда не мог понять, откуда берется существование этого всего. Сумм, свободных монад...

Date: 2016-10-25 10:57 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
В каком смысле оно всё есть в Хаскеле я сам не понимаю, категорию Hask пока никто не определил; я читаю эти статьи и их результаты через призму того, как те же конструкции имплементировались бы в чистой MLTT и какая бы у них получалась семантика в её естественных моделях (собственно синтаксическая категория и элементарные топосы с NNO), и там и там это всё понятно как работает и откуда берётся.

Хотя и тут, конечно, есть аспект: хочется сразу смотреть, как именно оно работает в HoTT, а не в ETT. Синтаксис я там хорошо понимаю, а семантику более или менее разобрал только в одной конкретной модели — модели Воеводского-Капулькина в симплициальных множествах, что меня категорически не устраивает, т.к. это неконструктивная модель. Есть, конечно, результаты, указывающие на то, что неконструктивность можно починить (https://arxiv.org/pdf/1510.00669.pdf, исходная статья Gambino + Sattler, последняя версия от конца сентября сего года содержит новые результаты by Coquand + Joyal), однако это work in progress, и для меня пока совершенно непрозрачно как там чего в деталях работает.

Но я надеюсь придёт тот день, когда у нас будут нормальные определения для элементарных и арифметических (∞, 1)-топосов, нормальная интуиция по поводу того как они работают и верифицированная теорема, что внутренним языком первых является минимальная HoTT c унивалентными вселенными и HoTT с унивалентными вселенными и всеми индуктивными типами соответственно.

Date: 2016-10-25 08:50 am (UTC)
From: [identity profile] clayrat.livejournal.com
а идрисовы эффекты видели? https://eb.host.cs.st-andrews.ac.uk/drafts/effects.pdf

Date: 2016-10-25 09:16 am (UTC)
From: [identity profile] maxim.livejournal.com
+1 реквестирую анализ эффектов идриса, а также http://eff-lang.org и олсо http://tomasp.net/coeffects/

Date: 2016-10-25 11:08 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Eff Lang (и МакБрайдовский Frank) — просто языки с нативной поддержкой алгебраических эффектов, библиотека Киселёва et al. это просто механизм для их интерпретации в чистый язык. А вот коэффекты эта штука никак не реализует.

Date: 2016-10-25 11:26 am (UTC)
From: [identity profile] maxim.livejournal.com
Так а ты писал когда-то про коэффекты, я помню.

Date: 2016-10-25 02:13 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Да, эта тема меня жутко интересует, но это work-in-progress, я пока не понимаю как следует как нужно понимать коэффекты. Для понимания коэффектов мне кажется ключевым образом важным как раз понять, как энфорсить контракты на эффекты. Возьмём условный язык (на основе Frank'а) где есть нативная поддержка эффектов, т.е. термы могут иметь чистую сигнатуру t(x : X) : Y, а могут нечистую
t(x : X) @PerformsIO @Throws[IllegalInputException] Y, а эффекты представляют из собой набор команд, снабженных сигнатурой:

@Effect PerformsIO:
  say(s : Message) @PerformsIO Unit
  ask(q : Question) @PerformsIO q.Response

@Effect Throws[E : ∗]:
  throw(e : E) @Throws[E] ⊥


Благодаря Киселёву, у них есть понятная монадная семантика. Сигнатуры эффектов превращаются в индуктивные типа
data PerformsIO : * -> * where
  say(s : Message) : PerformsIO Unit
  ask(q : Question) : PerformsIO (responseT q)


А потом для любого списка эффектов делается монада Eff '[PerformsIO, Throws E], и процыдурки обретают чистый тип X -> Eff '[PerformsIO, Throws E] Y.

Как это работает для коэффектов я пока в точности не понимаю.

Date: 2016-10-26 03:57 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Т.е. такая вот сигнатура эффекта на самом деле обычно (необходимым условием является, например, отсутствие команд типа throw, возвращающих ⊥) допускает реализацию эффекта и в комонадическом варианте*, т.е. процедура типа t(x : X) @PerformsIO Y допускает интерпретацию как t (x : X, h :: IoHandler) : Y, где IoHandler представляет собой изолированный аффинный stateful объект, предоставляющий методы say и ask заданной сигнатуры; изолированость означает в терминах императивных языков, что этот объект живёт в стеке, ссылки на него нельзя передавать на сторону и клонированию он не подлежит.

Разница между монадической и комонадической реализацией в том, как устроены хэндлеры. Хендлеры монадического типа устроены как обобщенные ловилки эксепшенов catch(e : Exception, resume :: Continuation), т.е. ловят событие “была инвоукнута команда” ниже вдоль control flow, и получают continuation в качестве изолированного аффинного аргумента, они его могут вызывать, могут не вызывать, могут вызывать потом, что-нибудь поделав сперва, но (как и выше) не могут его клонировать или передавать ссылки на него на сторону, что гарантирует что два раза оно не вызовется. Получается, что монадические хендлеры могут влиять на control flow начиная с точки их срабатывания, причём наиболее общим способом. Комонадические хендлеры поставляются в процедуру со стороны контекста, т.е. определены выше по control flow, влиять на него они никак не могут, по двойственности они могут что-то такое “зато” но я не знаю, что именно.

Вот на уровне сигнатур всё интересно, можно легко представить себе сигнатуры эффектов, допускающие только комонадическую, но не монадическую реализацию — это команды, влияющие на то, какие команды доступны после их вызова (т.е. меняющие тип своего h : EffectHandler) в процессе работы, что позволяет делать, например, одноразовые getter'ы. Именно так при помощи эффектов можно эмулировать афинные типы (кажется, это аффинные типы не такого рода как в линейной логике, а того который нужен для Session Types и типизированного кооперативного мультитрединга).

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

Жопой чую Интуиция подсказывает, что если научиться понимать как энфорсить на сигнатуры эффектов условия вроде коммутирования команд и указывать для команд спецификации в виде predicate transformers, и всё станет понятно с этими комонадическими эффектами, т.к. это проявит (несимметричное) влияние information flow на двойственные друг другу монадическую и комонадическую структуры.

Ещё очень хочется понять как в этом фреймворке красиво представить тот или иной вариант Actor Model/CSP.

(* Расшифрую “допускает реализацию в комонадическом варианте”: Сигнатура позволяет построить не только свободную монаду Eff, но и косвободную комонаду левосопряженную Eff, что означает, что Клейсли категория первой канонически изоморфна коКлейсли категории второй, т.е. в терминах стрелок они описывают ровно одинаковые эффекты.)

Date: 2016-10-26 08:50 am (UTC)
From: [identity profile] maxim.livejournal.com
Так как я не математик, то я буду на пальцах как инженер-обезьяна.
Как я вижу эффекты. Вот эффекты используемые в промышленности.

exception : rise
       io : read, write
    state : get, put
     comm : send, recv
      rnd : next


Всех их объединяет единственный интерфейс Get/Put (положить или взять из среды). Большинство хендлеров симметричны, но эксепшин например может только ложить в среду, а рендом только брать из среды. Эффекты всегда точки, т.е. -- это oneshot футуры, или элементарные poll стримов.

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

P.S. вот я пытался для EXE портировать систему эффектов идриса http://groupoid.space/types.htm#effect
Edited Date: 2016-10-26 08:50 am (UTC)

Date: 2016-10-28 01:43 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Вот я собственно и встречал только два класса эффектов — те, которые oneshot и специфицируются предикаттрансформером, и эффекты, касающиеся Actor Model/CSP. И я не понимаю как правильно описывать CSP, но мне почему-то кажется, что это типотеоретическая реализация темпоральной логики должна быть, а темпоральная логика как и всякая модальная логика вся в interplay between a pair of dual modal operators, а эти самые двойственные модальные операторы — это монадическое и комонадическое представление одного и того же явления.

Date: 2016-10-28 04:17 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Вот я собственно и встречал только два класса эффектов — те, которые oneshot и специфицируются предикаттрансформером, и эффекты, касающиеся Actor Model/CSP. И я не понимаю как правильно описывать CSP, но мне почему-то кажется, что это типотеоретическая реализация темпоральной логики должна быть, а темпоральная логика как и всякая модальная логика вся в interplay between a pair of dual modal operators, а эти самые двойственные модальные операторы — это монадическое и комонадическое представление одного и того же явления.

Date: 2016-10-25 11:01 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Да. По модулю более удобного нативного синтаксиса это (как и претнаровский Eff-lang и макбрайдовский Frank) ровно то, что у Киселёва et al.

Date: 2016-10-25 08:01 pm (UTC)
From: [identity profile] max630.livejournal.com
> На чистом хаскеле безо всяких макросов

это немного преувеличение, там внутри не обошлось без Data.Typeable

Date: 2016-10-25 11:48 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
О, ОК, всё-таки немножко метапрограммирования использовали. Видимо в определении open union...

Date: 2016-10-31 07:37 pm (UTC)
From: [identity profile] roman 3237465 (from livejournal.com)
>Кажется, там ничего не сломается, кроме того что Eff станет вообще говоря относительной монадой (“монадоподобный объект, не являющийся эндофунктором”).
Трансформером эффектов и Hoare state monad: https://github.com/effectfully/Eff

Data.Typeable там нет. Он был в оригинальных extensible effects.
Page generated Sep. 21st, 2017 03:42 pm
Powered by Dreamwidth Studios