Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Okmij

Вчера у меня наконец дошли руки посмотреть на статью 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 коммутировали), я вообще пока не встречал удовлетворительного подхода к этому вопросу, если работать в терминах монад/комонад, а не в терминах стрелок. Но по идее оно должно быть, собственно монадами описываются эффекты, у которых контракты накладываются на интерпретатор (если он есть), а процедуры могут полагаться на их выполнение, а комонадами эффекты, налагающие на использующую их процедуру обязательства по выполнению контрактов (например, использовать вызов команды только один раз).
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 14 comments

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…