Seguramente se lo han preguntado, si esta tan bueno dependently typed, porque no lo implementa Haskell?
El problema es que debería romper la restricción de fase entre el tipo y niveles de valor que permite Haskell para ser compilado a código máquina eficiente. Con nuestro nivel actual de la tecnología, un lenguaje dependently typed debe correr sobre una maquina virtual o interprete.
Idris es compila a C pero tiene un garage collector, la verdad no se bien como lo hace. Alguien me ayuda?
Translate
Mostrando las entradas con la etiqueta Dependent type. Mostrar todas las entradas
Mostrando las entradas con la etiqueta Dependent type. Mostrar todas las entradas
lunes, 20 de junio de 2016
domingo, 15 de diciembre de 2013
Idris, un lenguaje de programación con Dependent type
Idris es un lenguaje funcional de propósito general, con una particularidad es un lenguaje con Dependent type. Ahora viene la pregunta ¿que es Dependent type? Dependent type es un concepto de la programación pero también de la lógica; Dependent type es un tipo que depende de un valor. En la programación funcional se utiliza para prevenir errores, al permitir un sistema de tipo extensivo.
Dependent type añaden complejidad a un sistema de tipos. Es decir, para saber un tipo en algunos casos se deben realizar cálculos o ejecutar sentencias; esto hace bastante complejo el proceso de chequeo de tipos; y en algunos casos imposible. Pero algunos aspectos del comportamiento de un programa se pueden especificar con precisión en el tipo.
Idris es un lenguaje muy similar a haskell; pero con la propiedad de Dependent type.
Dejo links:
http://www.idris-lang.org/
Suscribirse a:
Entradas (Atom)