Lenguajes similares Haskell: Agda
Agda es un lenguaje de programación funcional con tipado dependiente. Donde los tipos pueden depender de valores, lo que permite expresar invariantes directamente en el sistema de tipos.
Es una extensión de la teoría de tipos de Martin-Löf y representa el desarrollo más reciente de lenguajes creados en el grupo de lógica de programación de Chalmers.
"Gracias a su fuerte tipado y a los tipos dependientes, Agda puede utilizarse como asistente de demostración, lo que permite probar teoremas matemáticos (en un entorno constructivo) y ejecutar dichas pruebas como algoritmos".
Además de programar, puedes demostrar teoremas y verificar que tu código cumple propiedades matemáticas.
Se usa principalmente con Emacs, que ofrece asistencia paso a paso para escribir programas y pruebas.
La similitud con Haskell coniste en compartir la orientación funcional, pero Agda va más allá al integrar la lógica formal en el lenguaje.
Comparativa con Haskell
Observemos la siguiente tabla comparativa
| Aspecto | Haskell | Agda |
|---|---|---|
| Tipos | Fuertes y estáticos, con soporte para GADTs | Dependientes: los tipos pueden depender de valores |
| Propósito | Programación general | Programación + demostración de teoremas |
| Entorno | GHC, Stack, Cabal | Emacs + asistente interactivo |
| Paradigma | Funcional puro | Funcional + lógico (constructivista) |
| Uso común | Aplicaciones, librerías, investigación | Verificación formal, matemáticas constructivas |
Instalando Agda
Para instalarlo requerimos tener Cabal instalado: https://www.haskell.org/cabal/
Abrimos una terminal y tecleamos:
$ cabal update $ cabal install Agda --v
Un vistazo al lenguaje Agda
Para conocer un poco este lenguaje no hay nada mejor que hacer el clásico programa de "Hola, mundo".
HolaMundo.agda
module HolaMundo where open import IO open import Data.String main : IO Unit main = putStrLn "Hola, mundo"
Como se puede ver, un programa en Agda tiene la extensión *.adga.
Compilación:
$ agda --compile HolaMundo.agda
Esto creará un ejecutable cuya salida será:
Hola, mundo
Y que tal un programa que sume dos números naturales enteros.
Suma.agda
open import Agda.Builtin.Nat open import Agda.Builtin.IO open import Agda.Builtin.Unit add : Nat → Nat → Nat add x y = x + y main : IO Unit main = putStrLn (show (add 3 4)) -- Resultado: 7
Compilación:
$ agda --compile Suma.agda
Esto creará un ejecutable cuya salida será:
7
Por el momento es todo. Continuaremos hablando de estos lenguajes similares a Haskell e próximas entregas.
Enlaces:
https://agda.readthedocs.io/en/v2.8.0-r3/https://alquimistadecodigo.blogspot.com/2026/02/nuevos-lenguajes-de-programacion.html https://www.haskell.org/cabal/
Comentarios
Publicar un comentario