paf31 / 24-days-of-purescript-2016

Dependentele functionale au aterizat in versiunea compilatorului 0.10.1. La inceput, dependentele functionale par o caracteristica relativ avansata a verificatorului de tip, cu unele consecinte placute pentru calitatea inferentei de tip si a mesajelor de eroare. Dar dependentele functionale sunt mult mai multe decat acestea – reprezinta primii pasi spre a permite o programare bogata la nivel de tip in PureScript.

Pentru a demonstra de ce dependentele functionale sunt interesante, voi arata cateva exemple de cod care au aparut in scurt timp de cand au fost adaugate dependentele functionale.

Dar mai intai, sa ne reamintim o caracteristica de sistem de tip mai simplu: clasele de tip multi-parametru.

Clase de tip multi-parametru

Clasele de tipuri ale unui argument reprezinta predicate pe tipuri.

De exemplu, clasa Eq reprezinta predicatul care afirma ca un tip are egalitate decisiva. Functia eq definita de clasa Eq este dovada acestei afirmatii.

Dar PureScript nu este limitat la clasele de tipuri ale unui singur argument. Clasele de tipuri pot avea zero sau mai multe argumente de tip.

Clasele de tip fara argumente (sau clase de tip nulare ) reprezinta afirmatii . De exemplu, clasa Partiala reprezinta afirmatia ca dezvoltatorul este constient ca foloseste functii partiale.

Clasele de tipuri cu doua sau mai multe argumente de tip reprezinta relatii intre tipuri. De exemplu:

• Clasa MonadEff reprezinta o relatie intre o monada si efectele pe care le gestioneaza prin intermediul monadei Eff.
• Clasa Paralel reprezinta o relatie intre o monada si un functor aplicativ, astfel incat putem folosi functia aplicativa pentru a executa comenzi in paralel.

Relatii si functii

Dar multe clase de tip cu argumente de tip multiplu reprezinta mai mult decat simple relatii. Mai multe clase de tip reprezinta functii intre tipuri. Dependentele functionale ne permit sa surprindem aceste tipuri de relatii intre argumentele de tip:

• In cazul MonadEff, ne putem gandi la relatia dintre o monada si randul sau de efecte ca la o functie – monada determina randul efectului in mod unic.
• Clasa paralela reprezinta o corespondenta intre monade si functori aplicativi. Fiecare parte a perechii o determina pe cealalta in mod unic.

Acum putem scrie:

pentru a afirma ca relatia dintre tipuri este functionala intr-una sau mai multe directii.

Inainte de 0.10.1, nu aveam nicio modalitate de a comunica aceste informatii verificatorului de tip. Dar acum, verificatorul de tip poate folosi aceste informatii pentru a ajuta la deducerea tipului sau pentru a furniza mesaje de eroare mai bune.

De exemplu, daca verificatorul de tip cunoaste monada m intr-o constrangere MonadEff eff m, atunci nu este necesar sa stie eff, deoarece m determina eff datorita dependentei functionale. Astfel, compilatorul se poate angaja sa aleaga instanta si sa completeze tipul corespunzator pentru eff, pe baza tipului m.

Daca ati intalnit vreodata tipuri de erori care au iesit din verificatorul de tip inainte de 0.10.1 cand utilizati transformatoare monad, atunci ar trebui sa apreciati acest tip de inferenta in cel mai recent compilator!

Aplicatii

Iata cateva dintre lucrurile care au fost deja construite folosind dependente functionale:

Liste indexate pe lungime (@bodil)

La scurt timp dupa lansarea 0.10.1, @bodil a lansat biblioteca purescript-typelevel, care continea o definitie a numerelor naturale la nivel de tip si a folosit dependente functionale pentru a exprima functii intre ele.

Biblioteca permite utilizatorului sa adauge, sa scada, sa inmulteasca, sa imparta si sa compare numere naturale la nivel de tip. Si amintiti-va ca toate aceste calcule au loc in interiorul verificatorului de tip in timpul compilarii!

Folosind numere naturale la nivel de tip, este posibil sa se defineasca un tip de liste (sau vectori ) indexate pe lungime . Acestea sunt furnizate de biblioteca vectorilor de dimensiuni purescript @ bodil.

De exemplu, biblioteca ofera urmatorul tip functiei de concatenare a listei:

Acest tip codifica invariantul pe care il adauga lungimile pe masura ce concatenam vectori. Si folosind dependente functionale, compilatorul poate calcula lungimea rezultatului din lungimile intrarilor.

Acest lucru ne permite sa facem afirmatii cu privire la lungimile listelor in timpul compilarii, evitand erori in afara intervalului.

Tip-nivel 2-3 copaci (@LiamGoodacre)

@LiamGoodacre a implementat recent harti la nivel de tip, de la simboluri (siruri la nivel de tip) pana la tipuri, ca arbori la nivel de tip 2-3 in biblioteca sa de harti de tip purescript.

Aceasta biblioteca ar putea oferi baza pentru o alternativa interesanta la polimorfismul randurilor, permitandu-ne sa vorbim despre randuri de tipuri folosind dependente functionale. De fapt, acest tip de abordare ne-ar putea permite sa afirmam afirmatii mult mai interesante despre randuri decat sistemul curent, deoarece avem un intreg limbaj complet Turing la nivelul tipului cu care putem lucra.

Calcul de tip Lambda la nivel (@LiamGoodacre)

Daca nu sunteti convins ca dependentele functionale ne ofera un limbaj complet Turing pentru programarea la nivel de tip, atunci aruncati o privire la acest interpret de calcul lambda, implementat in sistemul de tip folosind dependente functionale, de asemenea de @LiamGoodacre.

Acest sistem permite utilizatorului sa scrie orice termen de calcul lambda la nivel de tip, inclusiv abstractizari si aplicatii. Unele primitive, cum ar fi sirurile de nivel de tip si booleanele, sunt, de asemenea, acceptate. Apoi, putem evalua acesti termeni in forma normala la momentul compilarii in interiorul verificatorului de tip!

Am putea folosi acest lucru pentru a scrie programe arbitrare pentru a valida afirmatiile noastre cu privire la valorile din tipurile noastre (desi a face acest lucru in acest moment ar fi destul de greoi!)

Concluzie

Sper ca am aratat ca dependentele functionale imbunatatesc considerabil suportul pentru programarea la nivel de tip in compilator. Maine voi arata o aplicatie practica a dependentelor functionale in bibliotecile de baza.