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 :
