Agda come linguaggio di programmazione

Question

Ho trovato molte informazioni utili sull'uso di Agda come sistema di prova. Non ho trovato praticamente nessuna informazione sull'uso di Agda per scrivere programmi utilizzabili. Non riesco nemmeno a trovare un esempio di "ciao mondo" che compaia con la versione più recente di Agda.

Quindi,

1. Ci sono buoni tutorial su Agda come un linguaggio di programmazione?

2. Esistono altri linguaggi di natura simile (lazy functional tipically typed) che hanno una documentazione più matura per utilizzarli come linguaggio di programmazione? (Ho trovato tonnellate di grande documentazione su Coq, ma, ancora, niente "Hello World").

Answer 1

Per stampare una stringa in Agda, è necessario il std lib. È possibile trovare un esempio di "ciao mondo" here per Agda 2.2.6 e std lib 0.3. Questo esempio non funziona con Agda corrente 2.3.0 e std lib 0.6. Ho letto alcune fonti in std lib 0.6, e trovo che il seguente uno lavora:

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!") 

per compilarlo, è necessario

1. salvarlo a "./hello.agda"
2. scaricare lib-0.6.tar.gz e scompattarlo da qualche parte, dicono DIR
3. cd DIR/ffi & & cabala installare
4. agda -i DIR/src -i. -c ciao.agda

Su MacOSX Lion con ghc-7.4.2 e cabal-1.16.0, questo esempio funziona correttamente. Ricevo un programma eseguibile denominato "ciao" con dimensione 19.1M.

Answer 2

Questo è nascente, ma un giorno potrebbe diventare una risorsa utile:

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