Jak opisuje się kontrakty futures w kategoriach teorii kategorii?

Odpowiedzi:

25

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. TheA

return:AAbind:(AB)AB
returnbindafBPromises / 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 .AAAλ

Najprostszą rzeczą, jaką możesz zrobić, jest zabranie , z tego powodu, że kiedy masz , zawsze masz. To działa, ale jest trochę nudne, IMO. :)AAA

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ą.AStreamAA

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.λ

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
1
Chciałbym dostać kopię tego, kiedy skończysz.
Dave Clarke
1
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 :)ZAZA
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