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 коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 20th, 2017 10:28 pm
Powered by Dreamwidth Studios