Limbajul de programare Epigram

Epigram
Epigram
Paradigmă	Funcțională
Apărut în	2004
Proiectat de	Conor McBride și James McKinna
Dezvoltator	Unmaintained
Ultima versiune	1
Tipare	static, dependent
Influențat de	ALF
Influențe	Agda, Idris
Sistem de operare	Cross-platform: Linux, Windows, Mac OS X
Licență	MIT
Prezență online	site web oficial

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ă

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:

Exemple

Numerele naturale

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:

${\underline {\mathrm {data} }}\;\left({\frac {}{{\mathsf {Nat}}:\star }}\right)\;{\underline {\mathrm {where} }}\;\left({\frac {}{{\mathsf {zero}}:{\mathsf {Nat}}}}\right)\;;\;\left({\frac {n:{\mathsf {Nat}}}{{\mathsf {suc}}\ n:{\mathsf {Nat}}}}\right)$

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 naturale

${\mathsf {NatInd}}:{\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow \star \Rightarrow P\ {\mathsf {zero}}\rightarrow \\(\forall n:{\mathsf {Nat}}\Rightarrow P\ n\rightarrow P\ ({\mathsf {suc}}\ n))\rightarrow \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}$

${\mathsf {NatInd}}\ P\ mz\ ms\ {\mathsf {zero}}\equiv mz$

${\mathsf {NatInd}}\ P\ mz\ ms\ ({\mathsf {suc}}\ n)\equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)$

...Ș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)

Adunare

${\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {rec} }}\ x\ \{$

${\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {case} }}\ x\ \{$

${\mathsf {plus\ zero}}\ y\Rightarrow y$

$\quad \quad {\mathsf {plus}}\ ({\mathsf {suc}}\ x)\ y\Rightarrow suc\ ({\mathsf {plus}}\ x\ y)\ \}\ \}$

...Ș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 dependente

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 $\star$; tipurile sunt expresii arbitrare de tip $\star$, 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 $P\rightarrow Q$, $\forall x:P\Rightarrow Q$, $x$ este legat în $Q$ la valoarea pe care argumentul funcției (de tip $P$) ia în cele din urmă.

Legături externe

• EPSRC pe ALF, lego și conexe (versiune arhivată la 2006)
• Epigram 1 GitHub repo
• Epigram 2 GitHub repo