Epigrama (lenguaje de programación)

Lenguaje de programación funcional

Epigram es un lenguaje de programación funcional con tipos dependientes y un entorno de desarrollo integrado (IDE) que normalmente se incluye con el lenguaje. El sistema de tipos de Epigram es lo suficientemente fuerte como para expresar especificaciones de programas . El objetivo es respaldar una transición fluida desde la programación ordinaria a programas integrados y pruebas cuya corrección pueda ser verificada y certificada por el compilador . Epigram explota la correspondencia de Curry-Howard , también denominada principio de proposiciones como tipos , y se basa en la teoría de tipos intuicionista .

El prototipo de Epigram fue implementado por Conor McBride en base al 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 de forma gratuita junto con un manual de usuario, un tutorial y algo de material de referencia. El sistema se ha utilizado en Linux , Windows y macOS .

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

Sintaxis

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

Ejemplos

Los números naturales

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

( ! ( ! ( n : Nat ! datos !---------! donde !----------! ; !-----------! ! Nat : * ) ! cero : Nat ) ! suc n : Nat )                         

La declaración dice que Nates un tipo con clase * (es decir, es un tipo simple) y dos constructores: zeroy suc. El constructor suctoma un único Natargumento y devuelve un Nat. Esto es equivalente a la declaración de Haskelldata Nat = Zero | Suc Nat " ".

En LaTeX, el código se muestra como:

${\displaystyle {\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)}$

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

Recursión sobre números 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 \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}}$

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

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

...Y en ASCII:

IndNat : todos P : Nat -> * => P cero -> ( todos n : Nat => P n -> P ( suc n )) -> todos n : Nat => P n NatInd P mz ms cero => mz NatInd P mz ms ( suc n ) => ms n ( NatInd P mz ms n )                                                 

Suma

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

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

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

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

...Y en ASCII:

más  x  y <= rec x { más x y <= caso x { más cero y => y más ( suc x ) y => suc ( más x y ) } }                          

Tipos dependientes

Epigram es esencialmente un cálculo lambda tipado con extensiones de tipos de datos algebraicos generalizados , excepto por dos extensiones. Primero, los tipos son entidades de primera clase, de tipo ; los tipos son expresiones arbitrarias de tipo , y la equivalencia de tipos se define en términos de las formas normales de los tipos. Segundo, tiene un tipo de función dependiente; en lugar de , , donde está ligado al valor que el argumento de la función (de tipo ) eventualmente 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 de Dependent ML , los valores de los que dependen pueden ser de cualquier tipo válido). Se puede encontrar una muestra de las nuevas capacidades de especificación formal que brindan los tipos dependientes en el Tutorial de Epigram .

Véase también

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

Lectura adicional

• McBride, Conor; McKinna, James (2004). "La vista desde la izquierda". Revista de programación funcional . 14 : 69–111. doi : 10.1017/S0956796803004829 . S2CID  6232997.
• McBride, Conor (2004). El prototipo del epigrama, un guiño y dos guiños (Informe).
• McBride, Conor (2004). El tutorial de epigramas (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 verificador de tipos independiente para ETT (informe).
• Chapman, James; Dagand, Pierre-Évariste; McBride, Conor; Morris, Peter (2010). El delicado arte de la levitación (informe).

Referencias

1. «Epigrama – Sitio web oficial» . Consultado el 28 de noviembre de 2015 .

Enlaces externos

• Sitio web oficial
• Epigrama 1 en GitHub
• Epigram2 en GitHub
• EPSRC sobre ALF, lego y relacionados; versión archivada de 2006