Agda como lenguaje de programación [cerrado]

StackOverflow https://stackoverflow.com//questions/9692445

  •  13-12-2019
  •  | 
  •  

Pregunta

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

Entonces,

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

  2. ¿Existen otros lenguajes de naturaleza similar (funcionales diferidos escritos de forma dependiente) que tengan documentación más madura para usarlos como lenguaje de programación?(Encontré toneladas de documentación excelente sobre Coq, pero, nuevamente, nada de "Hola mundo").

¿Fue útil?

Solución

Para imprimir una cadena en Agda, necesita el biblioteca estándar.Puedes encontrar un ejemplo de "hola mundo" aquí para Agda 2.2.6 y std lib 0.3.Este ejemplo no funciona para Agda 2.3.0 y std lib 0.6 actuales.Leí algunas fuentes en std lib 0.6 y descubrí 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. guárdelo en "./hello.agda"
  2. descargue lib-0.6.tar.gz y descomprímalo en algún lugar, diga DIR
  3. instalación de cd DIR/ffi && cabal
  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.

Otros consejos

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

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

Licenciado bajo: CC-BY-SA con atribución
No afiliado a StackOverflow
scroll top