I have found a lot of useful information on using Agda as a proof system. I have found virtually no information on using Agda to write usable programs. I cannot even find a "hello world" example that compiles with the most recent version of Agda.
So,
Are there any good tutorials on Agda as a programming language?
Are there other languages of a similar nature (lazy functional dependently typed) that have more mature documentation for using them as a programming language? (I found tons of great documentation on Coq, but, again, no "Hello World").
To print a string in Agda, you need the std lib. You can find a "hello world" example here for Agda 2.2.6 and std lib 0.3. This example doesn't work for current Agda 2.3.0 and std lib 0.6. I read some sources in std lib 0.6, and find that the following one works:
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!")
To compile it, you need
On my MacOSX Lion with ghc-7.4.2 and cabal-1.16.0, this example works fine. I get an executable program named "hello" with size 19.1M.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With