Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

JoinadFix

Внезапно понял, что операции из вчерашнего поста следует называть join и reduce, причём join имеет прямое отношение к join calculus, прекрасному подходу к многопоточности без нелокальной синхронизации, близкому к Actor Model и линейной логике. Просто по всему выходит, что высший аналог MonadFix это в точности джойнада, допускающая интерпретацию join calculus. Соответственно, вчерашний пост проапдейтил. Коль скоро у меня любая монада с нулём тривиальным образом является джойнадой, выходит что в терминах последних можно интерпретировать наконец императивный код не только с мутабельным состоянием, вводом-выводом, исключениями и прочими delimited continuation passing, но и с использованием любой разумной многопоточности, не прибегающей (к нереализуемой физически) нелокальной синхронизации.

Вот я, кажется, и понял каким образом соотносятся эффекты и многопоточность.

Осталось, впрочем, понять, как выглядит аналог монады Дейкстры для джойнад. Снабжение монады монадой Дейкстры (монадическим трансформером предикатов) позволяет зафиксировать допустимое разнообразие операционных семантик, а значит рассуждать о том, что алгоритм корректен при выполнении любым допустимым интерпретатором. В случае джойнад там где-то должна всплывать темпоральная (в духе TLA) логика.
Subscribe
  • 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.
  • 12 comments