Jak opisuje się kontrakty futures w kategoriach teorii kategorii?

Czy istnieje przydatny opis przyszłości lub obietnic w kategoriach teorii kategorii? W szczególności, czym może być kategoryczny dualność Future?

pl.programming-languages ct.category-theory concurrency

— Aleksiej Romanow
źródło

Tak się składa, że piszę teraz o tym artykuł. IMO dobrym sposobem na myślenie o przyszłości lub obietnicach jest korespondencja Curry-Howarda dla logiki czasowej .

Zasadniczo koncepcja futures polega na tym, że jest to struktura danych reprezentująca trwające obliczenia i na której można synchronizować. W kategoriach logiki temporalnej, jest to operator ostatecznie . Ma strukturę monadyczną: , w którym ikra działania procesu, który wraca natychmiast jej argumentu, i tworzy nowy proces, który czeka na ' a wartość stosuje do tej wartości, a następnie czeka na -wartość przed powrotem. The $\Diamond A$

\begin{array}{lcl} r e t u r n & : & A \to ◊ A \\ b i n d & : & (A \to ◊ B) \to ◊ A \to ◊ B \end{array}

$\begin{array}{lcl} \mathrm{return} & : & A \to \Diamond A \\ \mathrm{bind} & : & (A \to \Diamond{B}) \to \Diamond{A} \to \Diamond{B} \end{array}$

r e t u r n

$\mathrm{return}$

b i n d

$\mathrm{bind}$

a

$a$

f

$f$

B

$B$ Promises / Propozycja dla CommonJS wywołuje operację monadic bind then, a Scala 2.10 po prostu daje jej standardowy interfejs monadic .

Podwójny operatorowi ostatecznie jest zawsze operator logiki temporalnej, która mówi, że w każdej chwili, masz . Kiedy przechodzisz od semantyki logiki czasowej Kripkego (gdzie właśnie modelujesz sprawdzalność) do semantyki kategorialnej -calculus (gdzie modelujesz również warunki / dowody lambda), okazuje się, że jest na to wiele sposobów . $\Diamond{A}$ $\Box{A}$ $A$ $\lambda$

Najprostszą rzeczą, jaką możesz zrobić, jest zabranie , z tego powodu, że kiedy masz , zawsze masz. To działa, ale jest trochę nudne, IMO. :) $\Box{A} \triangleq A$ $A$

Najbardziej naturalną rzeczą (IMO) do zrobienia jest wzięcie , co pozwala ci uzyskać (potencjalnie inny) w każdej chwili. Następnie możesz zobaczyć wspólny styl programowania reaktywnego (FRP) (po raz pierwszy zaproponowany przez Tarmo Uustalu i Varmo Vene ) jako styl programowania dualnego do monadycznego z przyszłością. $\Box{A} \triangleq \mathsf{Stream}\;A$ $A$

Jednak comonadic -calculus, jak sugerują, pomimo swojej elegancji, powoduje poważną utratę wyrazistości w stosunku do programowania wprost za pomocą strumieni, ponieważ kategoria wolnych węgielnic, których używają, okazuje się mieć za mało elementów globalnych, aby oznaczać wiele interesujących programów , szczególnie stałe punkty. $\lambda$

Nick Benton i ja argumentowaliśmy za programowaniem wprost za pomocą strumieni w naszym artykule Ultrametric Semantics of Reactive Programs . Następnie Alan Jeffrey zasugerował użycie LTL jako systemu typów w swoim artykule LTL typy FRP , co Wolfgang Jeltsch poczynił również w swoim artykule W kierunku wspólnej semantycznej kategorii dla logiki czasowej w czasie i programowania reakcji reaktywnych .

Różnicę między poglądem, jaki Nick i ja przyjmujemy, a tym, które przyjmują Alan i Wolfgang, najlepiej zrozumieć (IMO), porównując konstrukcję podaną w Birkedal i in. Pierwsze kroki w teorii syntetycznych domen strzeżonych: indeksowanie kroków w toposie drzew z papierem Alana. Topos drzew (preheaves nad liczbami naturalnymi uporządkowanymi według wielkości) jest bardzo podobny do kategorii przestrzeni ultrametrycznych, których użyliśmy Nick i ja, ale o wiele łatwiej jest je porównać z kategorią Alana (presheaves w dyskretnej kategorii czasu), ponieważ oba są preheaf kategorie.

Jeśli interesują Cię kontrakty terminowe przeznaczone specjalnie dla współbieżności, może warto przyjrzeć się CTL zamiast LTL. AFAIK, to obecnie niezbadane terytorium!

EDYCJA: oto link do wersji roboczej . Artykuł dotyczy głównie implementacji FRP na maszynie, więc język jest synchroniczny. Ale większość dyskusji na temat przyszłości / wydarzeń w sekcji 3.3 powinna zasadniczo dotyczyć również prawdziwie współbieżnych języków.

— Neel Krishnaswami
źródło

Chciałbym dostać kopię tego, kiedy skończysz.

— Dave Clarke

Wydaje się, że traci to ważną cechę przyszłości: po uzyskaniu wartości nie można jej zmienić. Spróbowałbym to wyrazić, przyjmując

jako aksjomat, ale nie tego chcemy, jeśli

oznacza strumień ... I chciałbym również kopię artykułu, gdy będzie gotowy :)

A \to ◻ A

$A \to \Box A$

◻

$\Box$

— Alexey Romanov,

Niedawno przeczytałem, że typ Scala Try[T]i Future[T]to podwójny, ale nie całkiem zrozumiał, co to oznacza / w jakim sensie.

— Giorgio