| Idris | |
|---|---|
| clase de idioma | Funcional |
| Apareció en | 2007 [3] [4] [5] |
| Autor | edwin brady |
| extensión de archivo | .idro.lidr |
| Liberar | Idris 2 versión 0.5.1 [1] (20 de septiembre de 2021 ) |
| sistema de tipos | soporte de tipo estricto , estático y dependiente |
| sido influenciado | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Licencia | BSD-3 |
| Sitio web | idris-lang.org |
Idris es un lenguaje de programación puro , total funcional de propósito general con una sintaxis similar a Haskell y soporte para tipos dependientes [6] . El sistema de tipos es similar al sistema de tipos de Agda .
El lenguaje admite pruebas automáticas comparables a Coq , incluido el soporte para tácticas, pero no se enfoca en ellas, sino que se posiciona como un lenguaje de programación de propósito general . Los objetivos de su creación: rendimiento "suficiente", facilidad de gestión de efectos secundarios y medios para implementar lenguajes específicos de dominio incrustables .
Implementado en Haskell , disponible como paquete Hackage [7] . El código fuente de Idris se compila en un conjunto de representaciones intermedias [8] , y de ellas en código C , que se ejecuta usando un recolector de basura de copia que usa el algoritmo Cheney . También se implementó oficialmente la capacidad de compilar en código JavaScript (incluso para Node.js ). Existen implementaciones de terceros de generadores de código para Java , JVM , CIL , Erlang , PHP y (limitadamente) LLVM .
El idioma lleva el nombre del dragón cantante Idris del programa de televisión infantil británico de 1970 Ivor the Tank Engine [9] .
El lenguaje combina características de los principales lenguajes de programación funcional populares con características prestadas de los sistemas de prueba automática, borrando efectivamente la línea entre las dos clases de lenguajes.
La segunda versión del lenguaje (lanzada en 2020, basada en la "teoría cuantitativa de tipos" [10] ) difiere significativamente de la primera: se ha agregado soporte completo para tipos lineales , el código se compila de forma predeterminada en Scheme , el compilador del lenguaje está escrito en el propio lenguaje .
La sintaxis del lenguaje (como la de Agda ) es cercana a la de Haskell [11] . ¡Hola , mundo! en Idris se ve así:
módulo principal main : IO () main = putStrLn "¡Hola, mundo!"Las diferencias entre este programa y su equivalente de Haskell son los dos puntos simples (en lugar de los dobles) en la firma de la función principal y la ausencia de la palabra "dónde" en la declaración del módulo.
Como la mayoría de los lenguajes de programación funcionales modernos, el lenguaje admite tipos de datos recursivos (definidos por inducción) y polimorfismo paramétrico . Dichos tipos se pueden definir como en la sintaxis tradicional "Haskell98":
datos Árbol a = Nodo ( Árbol a ) ( Árbol a ) | hoja unay en la sintaxis GADT más general:
datos Árbol : Tipo -> Tipo donde Nodo : Árbol a -> Árbol a -> Árbol a Hoja : a -> Árbol aPor medio de tipos dependientes , es posible, en la etapa de verificación de tipos, realizar cálculos que involucren los valores que parametrizan los tipos. El siguiente código define una lista con una longitud dada estáticamente, tradicionalmente llamada vector :
data Vect : Nat -> Tipo -> Tipo donde Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aEste tipo se puede utilizar así:
adición total : Vect na -> Vect ma -> Vect ( n + m ) a añadir Nil ys = ys añadir ( x :: xs ) ys = x :: añadir xs ysLa función añade un vector de melementos de tipo aa un vector de nelementos de tipo a. Debido a que el tipo exacto de los vectores de entrada depende de los valores que se conocen definitivamente en el momento de la compilación, el vector resultante contendrá exactamente (n + m)elementos de tipo a.
La palabra " total" invoca una comprobación de completitud de análisis contra , que, para evitar entrar en un bucle infinito , informará un error si la función no cubre todos los casos posibles de , o no se puede probar (automáticamente).
Otro ejemplo: suma por pares de dos vectores parametrizados por su longitud:
par totalAgregar : Num a = > Vect na -> Vect na -> Vect na parSuma Nil Nil = Nil parSuma ( x :: xs ) ( y :: ys ) = x + y :: parSuma xs ysNumsignifica que el tipo apertenece a la clase de tipo Num . La función pasa con éxito la verificación de tipo, el caso en que uno de los vectores tendrá el valor Nil, mientras que el segundo será un número, no puede suceder. El sistema de tipos comprueba en tiempo de compilación que la longitud de ambos vectores coincida. Esto simplifica el texto de la función, que ya no es necesaria para manejar este caso especial.
Los tipos dependientes son lo suficientemente potentes como para describir la mayoría de las propiedades de los programas, de modo que un programa Idris puede resultar invariable en tiempo de compilación. Esto convierte el lenguaje en un sistema de prueba interactivo .
Idris admite dos formas de trabajar con el sistema de prueba automática: escribiendo llamadas sucesivas a tácticas ( estilo Coq , mientras que el conjunto de tácticas disponibles no es tan rico como en Coq, pero se puede ampliar con herramientas de metaprogramación estándar ) o paso a paso. -Desarrollo de prueba paso a paso ( estilo Epigram y Agda ).