Idris (lenguaje de programación)

La sintaxis de Idris muestra muchas similitudes con la de Haskell. Un programa "hola mundo" en Idris podría verse así:

Módulo principalprincipal : IO () principal = putStrLn "¡Hola, mundo!"

Las únicas diferencias entre este programa y su equivalente en Haskell son el uso de un solo punto (en lugar de dos) en la firma de tipo de la función principal y la omisión de la palabra " where" en la declaración del módulo . ^{[ 8 ]}

Idris admite tipos de datos definidos inductivamente y polimorfismo paramétrico . Dichos tipos se pueden definir tanto en la sintaxis tradicional tipo Haskell 98 :

Datos Árbol a = Nodo ( Árbol a ) ( Árbol a ) | Hoja a 

o en una sintaxis más general similar a la de los tipos de datos algebraicos generalizados (GADT):

Árbol de datos : Tipo -> Tipo donde Nodo : Árbol a -> Árbol a -> Árbol a Hoja : a -> Árbol a 

Con los tipos dependientes , es posible que aparezcan valores en los tipos; en efecto, cualquier cálculo a nivel de valor puede realizarse durante la verificación de tipos . A continuación se define un tipo de listas cuyas longitudes se conocen antes de que se ejecute el programa, tradicionalmente llamadas vectores :

datos Vect : Nat -> Type -> Type donde Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect n a ) -> Vect ( n + 1 ) a 

Este tipo se puede utilizar de la siguiente manera:

agregar total : Vecto n a -> Vecto m a -> Vecto ( n + m ) a agregar Nil ys = ys agregar ( x :: xs ) ys = x :: agregar xs ys 

La función appendagrega un vector de melementos de tipo aa un vector de nelementos de tipo a. Dado que los tipos precisos de los vectores de entrada dependen de un valor, es posible estar seguro en tiempo de compilación de que el vector resultante tendrá exactamente ( n+ m) elementos de tipo a. La palabra " total" invoca al verificador de totalidad que informará un error si la función no cubre todos los casos posibles o no se puede probar (automáticamente) que no entra en un bucle infinito .

Otro ejemplo común es la suma por pares de dos vectores que están parametrizados en función de su longitud:

Total pairAdd : Num a => Vect n a -> Vect n a -> Vect n a pairAdd Nil Nil = Nil pairAdd ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ys 

NumLa letra a indica que el tipo a pertenece a la clase de tiposNum . Nótese que esta función sigue superando la comprobación de tipos como total, aunque no haya coincidencia de mayúsculas y minúsculas Nilen un vector y un número en el otro. Dado que el sistema de tipos puede demostrar que los vectores tienen la misma longitud, podemos estar seguros en tiempo de compilación de que no se producirá ninguna coincidencia de mayúsculas y minúsculas y no es necesario incluirla en la definición de la función.

Los tipos dependientes son lo suficientemente potentes como para codificar la mayoría de las propiedades de los programas, y un programa Idris puede demostrar invariantes en tiempo de compilación. Esto convierte a Idris en un asistente de demostración.

Existen dos formas estándar de interactuar con los asistentes de demostración: mediante la escritura de una serie de invocaciones tácticas ( estilo Rocq ) o mediante la elaboración interactiva de un término de demostración ( estilo Epigram -Agda). Idris admite ambos modos de interacción, aunque el conjunto de tácticas disponibles aún no es tan útil como el de Rocq.

Dado que Idris incluye un asistente de pruebas, los programas Idris pueden escribirse para pasar pruebas entre sí. Si se tratan de forma ingenua, dichas pruebas permanecen durante la ejecución. Idris busca evitar este problema eliminando de forma agresiva los términos no utilizados. ^{[ 9 ] [ 10 ]}

Por defecto, Idris genera código nativo a través de C. El otro backend oficialmente compatible genera JavaScript .