Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

JoinadFix

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

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

Осталось, впрочем, понять, как выглядит аналог монады Дейкстры для джойнад. Снабжение монады монадой Дейкстры (монадическим трансформером предикатов) позволяет зафиксировать допустимое разнообразие операционных семантик, а значит рассуждать о том, что алгоритм корректен при выполнении любым допустимым интерпретатором. В случае джойнад там где-то должна всплывать темпоральная (в духе TLA) логика.
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 12 comments