Practical Affine Types [Romanian]

Original in English by Jesse A. Tov

Tipuri practice afine

Jesse A. Tov şi Riccardo Pucella

În Proc. 38th ACM Symposium on Principles of Programming Languages (POPL’11), January 2011

„Alms” este un limbaj de programare cu scop general care suportă tipuri de practice afine. Pentru a oferi expresivitatea logicii liniare lui Girard, păstrând sistem de tip clar şi convenabil, Alms utilizează tipuri expresive care minimizează notaţie în timp ce maximizează polimorfismul între tipurile afine şi nelimitate.

O caracteristică cheie lui Alms este abilitatea de a introduce tipuri abstracte afine prin semnătura indicaţie ML-stil. În Alms, o interfata poate impune restricţii mai rigide de utilizare a resurselor decât restricţiile de utilizare principale ale punerii sale în aplicare. Această formă de consolidare permite tipului de sistem în mod natural şi direct să exprime o varietate de protocoale de gestionare a resurselor de la sisteme de tip cu destinaţie specială.

Vă prezentam două dovezi pentru a demonstra validitatea obiectivelor noastre de proiectare. În primul rând, introducem o implimentare a prototip de Alms şi discutăm despre programarea experienţei noastre în limbă. În al doilea rând, vom stabili soliditatea limbii de bază. Noi folosim, de asemenea, modelul de bază pentru a demonstra o teoremă principală de tipuri.

Disponibil:

Alms este, de asemenea, disponibil pe Hackage, şi poate fi instalată împreună cu instalare lui Alms, deşi aceasta nu poate fi cea mai recentă versiune şi ea ascunde exemple într-o locaţie obscură cum ar fi $HOME/.

Ghid pentru Alms

Noţiuni de bază

Alms cere GHC pentru a construi. Este cunoscut că lucrează cu GHC 7.0.2, şi probabil nu mai funcţionează cu GHC 6. (Dacă doriţi să-l încercaţi şi nu puteţi rula GHC 7, daţi-mi să ştiu şi poate voi încerca să fac ca el să lucreze cu versiunea 6.10.)

Cu condiţia că dispuneţi de GHC recent, pentru a construi pe UNIX ar trebui să fiţi suficient să tastaţi:

 % make

Acest lucru ar trebui să producă un executabil Alms din directorul curent,

Dacă acest lucru nu reuşeşte, poate fi, de asemenea, necesar să instalaţi în primul rînd pachetul liniilor de redactare (editline) sau să dezactivaţi editarea liniilor (Vă rugăm să consultaţi Probleme cu redactarea liniilor – Editline Trouble).

Pe Windows, construiţi cu Cabal: 

 > runghc Setup.hs configure > runghc Setup.hs build

Acest lucru produce un executabil în  dist\build\alms\alms.

Cabal ar trebui să funcţioneze pe UNIX, de asemenea, dar amestecînd Cabal asta produce drumuri ce duc la erori de linkuri, aşa că este, probabil, cel mai bine să alegeţi sau una sau alta.

Ce trebuie să încercaţi

Exemple din lucrare şi încă ceva ce se află în examples/ directory. Exemplele din secţiunea 2 a depunerii POPL sunt în:

    examples/ex60-popl-deposit.alms
    examples/ex61-popl-AfArray.alms
    examples/ex62-popl-AfArray-type-error.alms
    examples/ex63-popl-CapArray.alms
    examples/ex64-popl-CapLockArray.alms
    examples/ex65-popl-Fractional.alms
    examples/ex66-popl-RWLock.alms

Alte exemple notabile includ două implementări de tipuri de sesiune, o implementare lui Sutherland-Hodgman de tăiere a poligonului re-intrant (1974, Sutherland-Hodgman re-entrant polygon clipping) folosind tipuri de sesiune şi Berkeley Sockets API din lucrarea noastră ESOP nostru 2010 de hârtie (ESOP 2010 paper)

    lib/libsessiontype.alms
    lib/libsessiontype2.alms
    examples/session-types-polygons.alms
    lib/libsocketcap.alms

Serverul ecou din lucrarea noastră ESOP, care utilizează libsocketcap, este înăuntru. Pentru al încerca, conectaţi-vă la portul 10000, rulaţi:   

% ./alms examples/echoServer.alms 10000

Pentru a vă conecta la server ecou, puteţi rula

% ./alms examples/netcat.alms localhost 10000

de la un alt terminal.

Directorul de exemple conţine mult mai multe exemple, dintre care multe sunt mici, dar care demonstrează tipuri sau erori de contract – un comentariu în partea de sus a fiecărui exemplu, care spune ce de aşteptat. Rulaţi mai multe dintre exemple cu:

% make examples

Sau executaţi exemple ca testele de regresie (liniştit):

% make tests

Desigur, puteţi rula, de asemenea, interpretatorul în modul interactiv:

% ./alms

Aveţi posibilitatea să încărcaţi bibliotecile din linia de comandă astfel:

% ./alms -lsocketcap

Sau din cadrul REPL ca aceasta:

#- #load "libsocketcap"

În cele din urmă, poate fi util să ştiţi despre comanda # i pentru a întreba REPL cu privire la identificare:

    #- #i list Exn *    type +`a list : `a = (::) of `a * `a list | ([])   -- built-in
    module Exn   -- defined at lib/libbasis.alms:198:1-32
    type +`a * +`b : a ⋁ b   -- built-in
    val ( * ) : int → int → int   -- built-in

Sintaxa lucrării contra sintaxa ASCII

Limba aşa cum este prezentat în lucrare este credincioasă limbii ca pusă în aplicare, cu excepţia pentru problemele legate de imprimare calificată:

Când lucrarea spune. . .

apoi tastaţi. . . .

 

∀ ∃ λ μ

all ex fun mu

(Legători)

α β

'a 'b

(Variabile de tip nelimitat)

\/

(asociere calificativă)

± ⌽ + -

= 0 + -

(Diferenţe)

α β

`a `b

(Variabile de tipuri afine)

→ U   → A

-> -A>

(săgeţile nelimitate şi de o utilizare)

→ ⟨alfa⟩ ⊔ ⟨β⟩

-a,b>

(săgeată cu expresie calificativă)

Probleme cu linia de redactare

Linia de editare este activată în mod implicit prin REPL, care depinde de pachetul liniei de editare Cabal (editline Cabal package). Dacă se produce o eraare şi spune ceva despre linia de editare, atunci există trei opţiuni:

  • Dezactivaţi linia de editare:

     % make clean; make FLAGS=-editline

    sau

    % cabal install --flags=-editline alms
  • Folosiţi în loc de aceasta linie de citire:

    % make clean; make FLAGS=readline

    sau

    % cabal install --flags=readline alms
  • Încercaţi să instalaţi linia de editare sau linie de citire. 

Instalarea liniei de editare poate fi sensibilă. Pe sistemul meu,

% cabal install editline

păre să-l instaleze, dar Cabal încă nu poate găsi aceasta la construirea acestui program. Instalarea liniei de editare la nivel global a făcut să aceasta să funcţioneze:

% sudo cabal install --global editline

(De asemenea, linia de citire nu a lucrat până când nu am instalat-o la nivel global.)

La acest punct, versiunile mai vechi ale Cabal pot da bibliotecii instalate permisiuni rele, de aceea aşa ceva ca acest lucru poate ajuta, în funcţie de locul în care se instalează:

% sudo chmod -R a+rX /usr/local/lib/editline*

Dacă instalarea de Cabala a pachetului GHC dă greş, poate fi necesar mai întâi să instalaţi biblioteca C, de care totul depinde. Sursă este disponibil la adresa http://. Pe sistemul meu Debian, am fost în stare să-l instalez cu: 

% sudo aptitude install libedit2 libedit-dev

Reţineţi că libeditline este o bibliotecă complet diferită, şi instalarea nu va ajuta.

ok ok