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
