documentation - language - Agda como lenguaje de programación

liquid lenguaje de programacion

Question

He encontrado mucha información útil sobre el uso de Agda como sistema de prueba. No he encontrado prácticamente ninguna información sobre el uso de Agda para escribir programas utilizables. Ni siquiera puedo encontrar un ejemplo de "hola mundo" que compile con la versión más reciente de Agda.

Asi que,

1. ¿Hay buenos tutoriales sobre Agda como lenguaje de programación?

2. ¿Existen otros lenguajes de naturaleza similar (con funcionalidad perezosa tipificada de manera dependiente) que tengan documentación más madura para usarlos como lenguaje de programación? (Encontré toneladas de gran documentación en Coq, pero, de nuevo, no hay "Hello World").

Answer 1

Esto es incipiente, pero un día podría convertirse en un recurso útil:

https://github.com/liamoc/learn-you-an-agda

Answer 2

Para imprimir una cadena en Agda, necesitas el std lib . Puede encontrar un ejemplo de "hola mundo" here para Agda 2.2.6 y std lib 0.3. Este ejemplo no funciona para Agda 2.3.0 actual y std lib 0.6. Leí algunas fuentes en std lib 0.6, y encuentro que la siguiente funciona:

module hello where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Foreign.Haskell using (Unit)

main : IO Unit
main = putStrLn (toCostring "Hello, Agda!")

Para compilarlo, necesitas

1. guardarlo en "./hello.agda"
2. descargue lib-0.6.tar.gz y descomprímalo en algún lugar, digamos DIR
3. cd DIR / ffi && cabal install
4. agda -i DIR / src -i. -c hola.agda

En mi MacOSX Lion con ghc-7.4.2 y cabal-1.16.0, este ejemplo funciona bien. Obtengo un programa ejecutable llamado "hola" con un tamaño de 19.1M.