Idris es un lenguaje de programación puramente funcional con tipos dependientes , evaluación perezosa opcional y características como un verificador de totalidad . Idris puede usarse como asistente de pruebas , pero está diseñado para ser un lenguaje de programación de propósito general similar a Haskell .
Paradigma | Funcional |
---|---|
Diseñada por | Edwin Brady |
Apareció por primera vez | 2007 [1] |
Lanzamiento estable | 1.3.3 [2] / 24 de mayo de 2020 |
Versión de vista previa | 0.3.0 (Idris 2) [3] / 13 de enero de 2021 |
SO | Multiplataforma |
Licencia | BSD |
Extensiones de nombre de archivo | .idr, .lidr |
Sitio web | idris-lang |
Influenciado por | |
Agda , Limpio , [4] Coq , [5] Epigrama , F # , Haskell , [5] ML , [5] Óxido [4] |
El sistema de tipos de Idris es similar al de Agda , y las demostraciones son similares al de Coq , incluidas las tácticas ( funciones / procedimientos de prueba de teoremas ) a través de la reflexión del elaborador. [6] En comparación con Agda y Coq, Idris prioriza la gestión de efectos secundarios y la compatibilidad con lenguajes específicos de dominio integrados . Idris compila en C (confiando en un recolector de basura de copia personalizado usando el algoritmo de Cheney ) y JavaScript (tanto en navegador como en Node.js ). Hay generadores de código de terceros para otras plataformas, incluidas JVM , CIL y LLVM . [7]
Idris lleva el nombre de un dragón cantor del programa de televisión infantil británico de los años 70 Ivor the Engine . [8]
Características
Idris combina una serie de características de lenguajes de programación funcional relativamente convencionales con características tomadas de asistentes de prueba .
Programación funcional
La sintaxis de Idris muestra muchas similitudes con la de Haskell. Un programa de hola mundo en Idris podría verse así:
módulo principalmain : IO ()
main = putStrLn "¡Hola, mundo!"
Las únicas diferencias entre este programa y su equivalente de Haskell son los dos puntos simples (en lugar de dobles) 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. [9]
Tipos de datos inductivos y paramétricos
Idris admite tipos de datos definidos inductivamente y polimorfismo paramétrico . Estos tipos se pueden definir en la sintaxis tradicional similar a " Haskell98 ":
árbol de datos a = Nodo ( árbol a ) ( árbol a ) | Hoja a
o en la sintaxis más general similar a GADT :
Árbol de datos : Tipo -> Tipo donde Nodo : Árbol a -> Árbol a -> Árbol una hoja : a -> Árbol a
Tipos dependientes
Con los tipos dependientes , es posible que aparezcan valores en los tipos; en efecto, cualquier cálculo a nivel de valor se puede realizar 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 -> Tipo -> Tipo donde Nil : Vect 0 a (: :) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) a
Este tipo se puede utilizar de la siguiente manera:
agregado total : Vect na -> Vect ma -> Vect ( n + m ) aañadir Nil ys = ysañadir ( x :: xs ) ys = x :: añadir xs ys
Las funciones añaden un vector de m elementos de tipo a a un vector de n elementos de tipo a. Dado que los tipos precisos de los vectores de entrada dependen de un valor, es posible tener la certeza 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 ingrese en un bucle infinito .
Otro ejemplo común es la suma por pares de dos vectores que están parametrizados sobre su longitud:
par total Agregar : Num a => Vect na -> Vect na -> Vect napar Agregar Nulo Nulo = Nulo
par Agregar ( x :: xs ) ( y :: ys ) = x + y :: par Agregar xs ys
Num a significa que el tipo a pertenece a la clase de tipo Num. Tenga en cuenta que esta función todavía se comprueba correctamente como total, aunque no hay ningún caso que coincida con Nil en un vector y un número en el otro. Dado que el sistema de tipos garantiza que ambos vectores tienen exactamente la misma longitud, podemos estar seguros en el momento de la compilación de que este caso no ocurrirá. Por lo tanto, no es necesario mencionarlo para que la función sea total.
Funciones del asistente de pruebas
Los tipos dependientes son lo suficientemente potentes como para codificar la mayoría de las propiedades de los programas, y un programa de Idris puede resultar invariante en tiempo de compilación. Esto convierte a Idris en un asistente de pruebas.
Hay dos formas estándar de interactuar con los asistentes de prueba: escribiendo una serie de invocaciones tácticas ( estilo Coq ) o elaborando interactivamente un término de prueba ( 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 Coq . [ vago ]
Codigo de GENERACION
Debido a que Idris contiene un asistente de pruebas, los programas de Idris se pueden escribir para pasar las pruebas. Si se tratan con ingenuidad, estas pruebas permanecen en tiempo de ejecución. Idris tiene como objetivo evitar este escollo borrando agresivamente los términos no utilizados. [10] [11]
Por defecto, Idris genera código nativo a través C . El otro backend con soporte oficial genera JavaScript .
Idris 2
Idris 2 es una nueva versión autohospedada del lenguaje que integra profundamente un sistema de tipos lineales , basado en la teoría de tipos cuantitativos . En la actualidad se compila en el Esquema y C . [12]
Ver también
- Programación funcional total
Referencias
- ^ Brady, Edwin (12 de diciembre de 2007). "Índice de / ~ eb / darcs / Idris" . Facultad de Ciencias de la Computación de la Universidad de St Andrews . Archivado desde el original el 20 de marzo de 2008.
- ^ "Versión 1.3.3" . Consultado el 25 de mayo de 2020 .
- ^ "Idris 2 versión 0.3.0 publicada" . www.idris-lang.org . Consultado el 17 de marzo de 2021 .
- ^ a b "Tipos de unicidad" . Idris 1.3.1 Documentación . Consultado el 26 de septiembre de 2019 .
- ^ a b c "Idris, una lengua con tipos dependientes" . Consultado el 26 de octubre de 2014 .
- ^ "Reflexión del elaborador - Documentación de Idris 1.3.2" . Consultado el 27 de abril de 2020 .
- ^ "Objetivos de generación de código - documentación de Idris 1.1.1" . docs.idris-lang.org .
- ^ "Preguntas frecuentes" . Consultado el 19 de julio de 2015 .
- ^ "Guía de sintaxis - documentación de Idris 1.3.2" . Consultado el 27 de abril de 2020 .
- ^ "Borrado por análisis de uso - documentación de Idris 1.1.1" . idris.readthedocs.org .
- ^ "Resultados de referencia" . ziman.functor.sk .
- ^ "idris-lang / Idris2" . GitHub . Consultado el 11 de abril de 2021 .
enlaces externos
- La página de inicio de Idris , que incluye documentación, preguntas frecuentes y ejemplos
- Idris en el repositorio de Hackage
- Documentación para Idris Language (tutorial, referencia de idioma, etc.)