🚀 go-pugleaf

Lucifer napisał:
> Tomasz Zielonka wrote:
> 
>> Gdyby chodziło Ci o logikę liniową
> 
> Padlo pojecie ktore chyba pierwszy raz widze, mozna jasniej?

W kontekście języków funkcyjnych powinienem raczej wspomnieć o typach
liniowych, które mają związek z logiką l. To znasz? Jeśli tak, to
trochę niepotrzebnie się rozpisałem :)

Nie jestem szczególnym znawcą w tej dziedzinie, ale spróbuję napisać o
co mniej więcej chodzi.



W różnych językach funkcyjnych różnie rozwiązuje się problem
destrukcyjnego uaktualniania stanu, wejścia/wyjścia, obiektów
mutowalnych (tablice, referencje) - jednym słowem mechanizmów
imperatywnych.

W językach gorliwych (SML, OCaml, Lisp, Scheme, Erlang, ...) najczęściej
po prostu udostępnia się takie mechanizmy w takiej samej lub podobnej
postaci jak w językach tradycyjnie uznawanych za imperatywne (Fortran,
C, Pascal).

W językach leniwych (Haskell, Clean) nie można tego zrobić tak po prostu
w ten sam sposób.

Głównym celem leniwości jest zwolnienie programisty z konieczności
określania czy i w jakiej kolejności mają być wykonywane poszczególne
obliczenia. Tu jest jeden problem - kolejność wykonywania operacji
imperatywnych przeważnie ma znaczenie. Przeglądarka WWW, która by
probowała odebrać odpowiedź z serwera jeszcze przed wysłaniem zapytania
byłaby raczej niezbyt użyteczna ;)

Drugi problem - języki funkcyjne mają umożliwiać, ułatwiać, a nawet
wymuszać sposób programowania, w którym obiekty na których się operuje
mają prostą, matematyczną semantykę wartości. W przypadku języka
imperatywnego można powiedzieć, że dana zmienna w pewnym momencie ma
wartość X, a w innym ma wartość Y, różną o X. W języku czysto-funkcyjnym
operuje się głównie na samych wartościach - wartościach niezmiennych,
więc takie stwierdzenie nie miałoby sensu.



Skupmy się na tablicach - jak można je efektywnie zaimplementować w
języku czysto-funkcyjnym? Przez "efektywnie" rozumiem stały
pesymistyczny koszt operacji update. Funkcja update bierze jako parametr
(tablica A, indeks I, wartość V), a jej wartością jest tablica, która,
oprócz tego, że na indeksie I ma wartość V, jest identyczna z tablicą A.

Wartości się nie zmienia, tylko produkuje nowe, zatem update nie może
tak po prostu zastosować podstawienia do wejściowej tablicy. No tak, ale
niezbyt efektywnie jest produkować nową tablicę za każdym razem, kiedy
się chce "zmienić" wartość pod jednym indeksem.

A gdyby mieć gwarancję, że "nikt już nie ruszy" wartości tablicy sprzed
zmiany? 

Można wtedy trochę oszukać i wykorzystać wejściową tablicę - wykonać na
niej imperatywne podstawienie i zwrócić jako wartość funkcji. I tak nikt
nie zauważy ;)

Typy liniowe pozwalają właśnie śledzić użycia wartości i umożliwiają
bezpieczne zastosowanie tej optymalizacji. Ich związek z
Intuicjonostyczną Logiką Liniową jest taki jak związek Konstruktywnej
Teorii Typów z Logiką Intuicjonostyczną (słyszał ktoś o izomorfizmie
Curriego-Howarda?).



Pewien wariant takiego podejście zastosowano w języku Clean, gdzie
nazywa się toto Uniqueness Typing. W Cleanie UT używa się standardowo
do I/O, operacji na mutowalnych tablicach i FFI. Sam wymyśliłem jeszcze
dwa zastosowania, jedno proste, drugie trochę bardziej ciekawe, ale nie
będę już nudził.

Zainteresowanych szczegółami odsyłam do:

  http://www.cs.kun.nl/~clean/
  http://www.research.avayalabs.com/user/wadler/topics/linear-logic.html



PS. Konkurencyjne podejście zastosowane w Haskellu opera się na
    monadach.

Pozdrawiam,
Tomek

-- 
.signature: Too many levels of symbolic links