Agda as a programming language [closed]
-
13-12-2019 - |
Question
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").
Solution
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
- save it to "./hello.agda"
- download lib-0.6.tar.gz, and unpack it to somewhere, say DIR
- cd DIR/ffi && cabal install
- agda -i DIR/src -i . -c hello.agda
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.
OTHER TIPS
This is nascent, but one-day might become a useful resource: