Porque Haskell no implementa dependently typed?

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?

Dependently typed languages

Existe una lucha en la oscuridad que nosotros poco conocemos entre tipado dinámico y estático. En cualquier sitio de programación se ven tablas comparativas con ventajas y desventajas de cada uno.

En el plano de la investigación hubo un gran adelanto en este tema con las teorías de dependently typed languages, que expanden los limites del tipado estático.

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.

Entre los lenguajes que implementan esta tecnica tenemos:

Agda: Agda es un lenguaje funcional con dependent typed. Es similar a Epigram pero con una sintaxis más parecida a Haskell-like syntax.

Idris: Lenguaje de proposito general muy parecido a haskell pero con  dependent typed

Cayenne: Este lenguaje fue influido por la teoría constructive type (pero eso es para otro post)

Que ventajas trae Dependently typed:
-Se pueden encontrar más errores en tiempo de compilación
-Editores que nos ayuden más
-Puede checkear que los elementos de tu programa estén bien.

Todo muy lindo, pero vamos con algo menos abstracto, vamos a ver una definición de tipo en Idris:

data Vect : Nat -> Type -> Type where
    Nil : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a

ufff, y yo pienso que mi vida es complicada...

Veamos, en la primera linea decimos, que definimos una familia de tipos que toman un Nat y retornan un tipo. Entonces le decimos cuando, en esta sentencia tiene que haber siempre al menos un verdadero. Es parecido a pattern maching pero con tipos.

Este tema es muy interesante voy a seguir con esto en futuros post.

Dejo link: https://wiki.haskell.org/Dependent_type

Seven More Languages in Seven Weeks: Languages That Are Shaping the Future

Alguna vez les hable del libro 7 lenguajes en 7 semanas, bueno las editorial The Pragmatic Bookshelf ha lanzado un nuevo libro con la misma temática. Los lenguajes a analizar son  Lua, Factor, Elm, Elixir, Julia, MiniKanren y Idris.

Y hasta tiene video y todo: 

Ya saben que regalarme!!

Dejo el link:
https://pragprog.com/book/7lang/seven-more-languages-in-seven-weeks

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/