Limbajul de programare Epigram

limbaj de programare
Epigram
ParadigmăFuncțională
Apărut în2004
Dezvoltat deConor McBride și
James McKinna
DeveloperUnmaintained
Ultima versiune1
Tipul de tipărirestatic, dependent
Influențat deALF
InfluențeAgda, Idris
Sistem de operareCross-platform: Linux, Windows, Mac OS X
LicențăMIT[1]

Epigram este un limbaj de programare funcțional cu tipuri dependente. Epigram se referă, de asemenea, la IDE, de obicei ambalate cu limba. Sistemul de tip Epigram este suficient de puternic pentru a exprima specificațiile programului. Scopul este de a sprijini o tranziție lină de la programele obișnuite la programele integrate și dovezile a căror corectitudine poate fi verificată și certificată de către compilator. Epigram exploatează propoziția ca principiu de tip și se bazează pe teoria tipului intuiționist.

Prototipul Epigram a fost implementat de Conor McBride pe baza colaborării cu James McKinna. Dezvoltarea sa este continuată de grupul Epigram din Nottingham, Durham, St Andrews și Royal Holloway din Marea Britanie. Actuala implementare experimentală a sistemului Epigram este disponibilă gratuit, împreună cu un manual de utilizare, un tutorial și un material de fond. Sistemul a fost folosit sub Linux, Windows și Mac OS X.

În prezent nu este disponibilă, iar versiunea 2, care a fost destinată implementării teoriei tipului observațional, nu a fost lansată oficial, totuși există o oglindă GitHub, actualizată ultima dată în 2012. Designul Epigram și Epigram 2 au inspirat dezvoltarea altor sisteme cum ar fi ca Agda, Idris și Coq.

SintaxăModificare

Epigram utilizează o sintaxă de stil deductibil în două dimensiuni, cu o versiune LaTeX și o versiune ASCII. Iată câteva exemple de la The Epigram Tutorial:

ExempleModificare

Numerele naturaleModificare

Următoarea declarație definește numerele naturale:

     (         !       (          !   (  n : Nat  !
data !---------! where !----------! ; !-----------!
     ! Nat : * )       !zero : Nat)   !suc n : Nat)

Declarația spune că Nat este un tip cu natură * (adică este un tip simplu) și doi constructori: zero și suc. Aceasta este echivalentă cu declarația Haskell "data Nat = Zero | Suc Nat".

La LaTeX, codul este afișat ca:

 

Notarea orizontală poate fi citită ca fiind "presupunând (ceea ce este pe partea de sus) este adevărat, putem deduce că (ceea ce este în partea de jos) este adevărat. "De exemplu," presupunând că n este de tip Nat, atunci suc n este de tip Nat. "Dacă nimic nu este pe partea de sus, atunci instrucțiunea de jos este întotdeauna adevărată:" zero este de tip Nat (în toate cazurile) ".

Recurgerea la naturaleModificare

 

 

 

...Și în ASCII:

NatInd : all P : Nat -> * => P zero ->
         (all n : Nat => P n -> P (suc n)) ->
         all n : Nat => P n
NatInd P mz ms zero => mz
NatInd P mz ms (suc n) => ms n (NatInd P mz ms n)

AdunareModificare

 
     
         
         

...Și în ASCII:

plus x y <= rec x {
  plus x y <= case x {
    plus zero y => y
    plus (suc x) y => suc (plus x y)
  }
}

Tipuri dependenteModificare

Epigrama este în esență un calcul lambda tipizat cu extensii generalizate de date algebrice, cu excepția a două extensii. În primul rând, tipurile sunt entități de primă clasă, de tip  ; tipurile sunt expresii arbitrare de tip  , iar tipul de echivalență este definit în termenii formelor normale ale tipurilor. În al doilea rând, are un tip de funcție dependentă; în loc de  ,  ,   este legat în   la valoarea pe care argumentul funcției (de tip  ) ia în cele din urmă.

NoteModificare

  1. ^ „epigram - Official website”. Accesat în . 

Legături externeModificare