Epigram (lenguaje de programación) - Epigram (programming language)

Epigrama

Paradigma	Funcional
Diseñada por	Conor McBride James McKinna
Desarrollador	Sin mantenimiento
Apareció por primera vez	2004 ; Hace 17 años  ( 2004 )
Lanzamiento estable	1/11 de octubre de 2006 ; hace 14 años  ( 11 de octubre de 2006 )
Disciplina de mecanografía	fuerte , estático , dependiente
SO	Multiplataforma : Linux , Windows , macOS
Licencia	MIT
Sitio web	web .archive .org / web / 20120717070845 / http: // www .e-pig .org / darcs / Pig09 / web /
Influenciado por
ALF
Influenciado
Agda , Idris

Epigram es un lenguaje de programación funcional con tipos dependientes y el entorno de desarrollo integrado (IDE) generalmente incluido con el lenguaje. El sistema de tipos de Epigram es lo suficientemente fuerte como para expresar las especificaciones del programa . El objetivo es apoyar una transición sin problemas de la programación ordinaria a programas integrados y pruebas cuya corrección puede ser verificada y certificada por el compilador . Epigram explota la correspondencia Curry-Howard , también denominada las proposiciones como principio de tipos , y se basa en la teoría de tipos intuicionista .

El prototipo de Epigram fue implementado por Conor McBride basado en el trabajo conjunto con James McKinna. Su desarrollo es continuado por el grupo Epigram en Nottingham , Durham , St Andrews y Royal Holloway, Universidad de Londres en el Reino Unido (UK). La implementación experimental actual del sistema Epigram está disponible gratuitamente junto con un manual de usuario, un tutorial y algún material de referencia. El sistema se ha utilizado en Linux , Windows y macOS .

Actualmente no se mantiene, y la versión 2, que estaba destinada a implementar la teoría de tipos observacionales, nunca se lanzó oficialmente, pero existe en GitHub .

Sintaxis

Epigram utiliza una sintaxis de estilo de deducción natural bidimensional , con versiones en LaTeX y ASCII . A continuación, se muestran algunos ejemplos del tutorial de Epigram :

Ejemplos de

Los números naturales

La siguiente declaración define los números naturales :

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

La declaración dice que Nat es un tipo con kind * (es decir, es un tipo simple) y dos constructores: zero y suc . El constructor suc toma un solo Nat argumento y devuelve un Nat . Esto es equivalente a la declaración de Haskell " data Nat = Zero | Suc Nat ".

En LaTeX, el código se muestra como:

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

La notación de línea horizontal se puede leer como "suponiendo que (lo que está en la parte superior) sea verdadero, podemos inferir que (lo que está en la parte inferior) es cierto". Por ejemplo, "asumiendo que n es de tipo Nat , entonces suc n es de tipo Nat ". Si no hay nada en la parte superior, entonces la declaración inferior siempre es verdadera: " zero es de tipo Nat (en todos los casos)".

Recurrencia en naturales

${\ Displaystyle {\ 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 \\\ para todos los n: {\ mathsf {Nat}} \ Rightarrow P \ n \ end {matriz}}}$

${\ Displaystyle {\ mathsf {NatInd}} \ P \ mz \ ms \ {\ mathsf {cero}} \ equiv mz}$

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

... Y en 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)

Adición

${\ Displaystyle {\ mathsf {más}} \ x \ y \ Leftarrow {\ underline {\ mathrm {rec}}} \ x \ \ {}$

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

${\ Displaystyle {\ mathsf {más \ cero}} \ y \ Rightarrow y}$

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

... Y en ASCII:

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

Tipos dependientes

Epigram es esencialmente un cálculo lambda tipificado con extensiones de tipo de datos algebraicos generalizados , excepto por dos extensiones. Primero, los tipos son entidades de primera clase, de tipo ; los tipos son expresiones arbitrarias de tipos y la equivalencia de tipos se define en términos de las formas normales de los tipos. En segundo lugar, tiene un tipo de función dependiente; en lugar de , donde se une en el valor que el argumento de la función (de tipo ) con el tiempo toma. ${\ Displaystyle \ star}$${\ Displaystyle \ star}$${\ Displaystyle P \ rightarrow Q}$${\ Displaystyle \ forall x: P \ Rightarrow Q}$${\ Displaystyle x}$${\ displaystyle Q}$${\ Displaystyle P}$

Los tipos totalmente dependientes, tal como se implementan en Epigram, son una abstracción poderosa. (A diferencia del ML dependiente , los valores de los que se depende pueden ser de cualquier tipo válido). En The Epigram Tutorial se puede encontrar una muestra de las nuevas capacidades de especificación formal que aportan los tipos dependientes .

Ver también

• ALF , un asistente de pruebas entre los predecesores de Epigram.

Otras lecturas

• McBride, Conor; McKinna, James (2004). "La vista desde la izquierda". Revista de programación funcional . 14 : 69-111. doi : 10.1017 / S0956796803004829 .
• McBride, Conor (2004). El prototipo Epigrama, un guiño y dos guiños (Informe).
• McBride, Conor (2004). El tutorial de Epigram (informe).
• Altenkirch, Thorsten; McBride, Conor; McKinna, James (2005). Por qué son importantes los tipos dependientes (informe).
• Chapman, James; Altenkirch, Thorsten; McBride, Conor (2006). Epigram Reloaded: un comprobador de tipos independiente para ETT (informe).
• Chapman, James; Dagand, Pierre-Évariste; McBride, Conor; Morris, Peter (2010). El suave arte de la levitación (Informe).

enlaces externos

• Página web oficial
• Epigrama 1 en GitHub
• Epigram2 en GitHub
• EPSRC en ALF, lego y afines; versión archivada de 2006

Referencias