JoinadFix

Nov. 13th, 2016 05:08 am
akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Внезапно понял, что операции из вчерашнего поста следует называть join и reduce, причём join имеет прямое отношение к join calculus, прекрасному подходу к многопоточности без нелокальной синхронизации, близкому к Actor Model и линейной логике. Просто по всему выходит, что высший аналог MonadFix это в точности джойнада, допускающая интерпретацию join calculus. Соответственно, вчерашний пост проапдейтил. Коль скоро у меня любая монада с нулём тривиальным образом является джойнадой, выходит что в терминах последних можно интерпретировать наконец императивный код не только с мутабельным состоянием, вводом-выводом, исключениями и прочими delimited continuation passing, но и с использованием любой разумной многопоточности, не прибегающей (к нереализуемой физически) нелокальной синхронизации.

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

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

Date: 2016-11-13 04:30 am (UTC)
From: [identity profile] chaource.livejournal.com
А я какъ разъ началъ разрабатывать библiотеку для Join Calculus на языкѣ Scala!

Почему-то Join Calculus въ индустрiи не используется совершенно нигдѣ. А вѣдь онъ гораздо понятнѣе и проще, чѣмъ Actor Model, которую какъ разъ уже иногда используютъ. Хотѣлось-бы понять, почему это, и какъ сдѣлать, чтобы Join Calculus использовали. Можетъ, нехватаетъ какихъ-то важныхъ для практическаго использованiя функцiй? Когда я разсказываю людямъ про Join Calculus, всѣ преисполняются энтузiазма.

Пока что я пишу документацiю и буду потомъ допиливать кодъ до индустрiальнаго состоянiя.
Edited Date: 2016-11-13 06:55 am (UTC)

Date: 2016-11-13 01:44 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
О, как мир-то тесен. Join Calculus волшебен. Мне он интересен с той точки зрения что очень близок (и, насколько я понимаю, эквивалентен Actor Model), и, что в отличие от pi-calculus и прочих СSP он не перехреначивает, а расширяет лямбда-исчисление, в результате примерно понятно как там делать зависимые типы в целом и статическую типизацию в частности, а там и до нормальной категорной семантики может дойти, это мне очень-очень интересно.

Actor Model на самом деле очень удобна, но ad-hoc'на. Мне хочется думать о типизированной модели экторов как о Join Calculus с Delimited Continuation Passing (что позволяет делать многоразовые каналы удобно).

Date: 2016-11-13 05:35 pm (UTC)
From: [identity profile] chaource.livejournal.com
А развѣ Join Calculus уже не содержитъ статическую типизацiю? Каждый каналъ принимаетъ значенiе только заданнаго типа.

Date: 2016-11-14 04:32 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Да, разумеется. Я как раз имел в виду, что статическая типизация там автоматически есть, и можно представить себе как там делать зависимые типы. Конечная цель, разумеется, в том, чтобы как в MLTT можно было при помощи типа “функции” сколь угодно строго описать её спецификацию.

Для чистых функций мы это умеем выражать спецификации типами делать в самой MLTT. Для процедур с эффектами, которые можно выразить при помощи монад, мы это умеем выражать спецификации, через монады Дейкстры (см. язык F*).

А вот для concurrent systems до сих пор толком не умеем. А хочется.

Date: 2016-11-13 08:19 am (UTC)
From: [identity profile] v256.livejournal.com
Join Calculus -- это такой CHR in disguise =)

Date: 2016-11-13 01:06 pm (UTC)
From: [identity profile] clayrat.livejournal.com
Constraint Handling Rules?

Date: 2016-11-13 01:50 pm (UTC)
From: [identity profile] v256.livejournal.com
Да. Вот и статья даже есть "Finally, A Comparison Between Constraint Handling Rules and Join-Calculus" by Edmund S L Lam and Martin Sulzmann

Date: 2016-11-13 01:52 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Ух ты, а спасибо за линк.

Date: 2016-11-14 06:57 am (UTC)
From: [identity profile] nivanych.livejournal.com
Ещё стоит обратить внимание на чууть другой путь "доработки лямбды", при помощи Update/Fusion Calculus.

Date: 2016-11-14 07:27 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Кажется, я как-то читал, и не впечатлися. Но я сейчас ещё раз посмотрю, может я как-то упустил суть, у меня иногда так бывает что на первый взгляд не оценил.

Date: 2016-11-14 08:16 pm (UTC)
From: [identity profile] nivanych.livejournal.com
Да в общем-то, это не есть уж совсем особенное, чтоб уж прям впечатлиться.
Это небольшое обобщение пи-исчисления.
Основная особенность — при "приёме сообщения", по умолчанию, переменная не биндится.
Поэтому, в каком-то смысле, основная операция больше похожа на что-то типа "присвоения".
Ну это я грубо описал, конечно.

Date: 2016-11-15 09:04 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Кажется, я как-то читал, и не впечатлися. Но я сейчас ещё раз посмотрю, может я как-то упустил суть, у меня иногда так бывает что на первый взгляд не оценил.
Page generated Sep. 21st, 2017 03:38 pm
Powered by Dreamwidth Studios