Solo Haskell: lo mejor es lo funcional

Koka es un lenguaje de programación funcional fuertemente tipado cuyo rasgo más distintivo es el uso de tipos de efectos (effect types) combinados con handlers. Es funcional (como Haskell). Tiene tipado estático fuerte. Pero además hace explícitos los efectos en los tipos. Relación con Haskell Koka y Haskell están muy relacionados conceptualmente: Aspecto Relación Paradigma Ambos son funcionales Tipado Ambos con tipado fuerte y avanzado Pureza Ambos promueven funciones puras Base teórica Comparten fundamentos (lambda calculus, tipos) Haskell: "los efectos están encapsulados en monadas". Koka: "los efectos forman parte del tipo". Instalando Koka Abrimos una terminal y tecleamos lo sigu...

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 Obse...