Agda

 Agda es un lenguaje funcional con dependently typed. Pero que es dependently typed? 

Te lo explico en este post : https://emanuelpeg.blogspot.com/2016/03/dependently-typed-languages.html

Pero si te da fiaca ir, te cuento: 

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.

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.

Agda se basa en la teoría de tipos intuicionista, un sistema fundamental para las matemáticas constructivas desarrollado por el lógico sueco Per Martin-Löf. Tiene muchas similitudes con otros lenguajes basados en dependently typed, como Coq, Epigram, Matita y NuPRL.

Agda es de código abierto y disfruta de las contribuciones de muchos autores. El centro del desarrollo de Agda es el grupo Programming Logic en Chalmers y la Universidad de Gotemburgo. Los principales desarrolladores son Ulf Norell, Nils Anders Danielsson, Andreas Abel y Jesper Cockx.

Vamos un pequeño ejemplo, definimos un tipo y luego la suma : 

data Nat : Set where

zero : Nat

suc : Nat -> Nat

_+_ : Nat -> Nat -> Nat

zero + m = m

suc n + m = suc (n + m)

y multiplicar : 

_*_ : Nat -> Nat -> Nat

zero * m = zero

suc n * m = m + n * m

Dejo link : 

https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html

https://github.com/agda/agda

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?

Learn You an Agda and Achieve Enlightenment!

Como todos tendemos a la iluminación les quiero recomendar esta pagina, en la cual nos enseñan sobre el lenguaje Agda. Para el que no leyó el post anterior Agda es un lenguaje funcional con dependently typed. A la vez esta muy emparentado con nuestro amigo Haskell. Por lo que es bueno tener nociones de Haskell antes de leer esta libro.

Sin más y esperando la iluminación, dejo link:
http://learnyouanagda.liamoc.net/

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