Agda as a Programming Language: Hello World

While checking out Agda, I found a lot of information on using Agda to prove things, but very little on using Agda to write programs. So I will post here what I learn, and maybe it will help someone.

As to why you would use Agda to write programs, well, I had a reason, but that's for another day.

Hello World

Agda keeps changing; the old Hello Worlds no longer compile (I have yet to find a single working example on the internet). After some struggle I managed to produce one:

     hello.agda 

  1  -- Compiles with Agda 2.3.0 and standard library 0.6
  2  -- on 2012-03-13
  3  
  4  module hello where
  5  
  6  open import IO.Primitive
  7  open import Data.String
  8  
  9  import Foreign.Haskell as Hask
 10  
 11  main : IO Hask.Unit
 12  main = putStrLn (toCostring "Hello, World!")

To run this program you will need:

• Agda 2.3.0
• Agda library 0.6

Both of these can be installed with cabal.

Then run:

  1  agda -i <path to standard library source> -i . -c hello.agda
  2  ./hello

So, in my case,

  1  agda -i ~/install/lib-0.6/src -i . -c hello.agda
  2  ./hello

Peculiarities of the program

• IO deals with Costrings rather than Strings (for some reason). A string literal is a String, so we convert it with toCostring. We could also have done:

    1  open import IO.Primitive renaming (putStrLn to putStrLnCo)
    2  
    3  putStrLn : String -> Hask.Unit
    4  putStrLn s = putStrLnCo (toCostring s)
  
  

• putStrLn is literally just the Haskell function of the same name; as such it returns Haskell's Unit type; Agda has its own Unit type (in Data.Unit), but these are not the same. So the result of main must be IO Foreign.Haskell.Unit.

• Agda has another IO library in IO; it might be better, but I didn't understand it, so I used IO.Primitive.

More IO

     someio.agda 

  1  module someio where
  2  
  3  import Foreign.Haskell as Hask
  4  open import IO.Primitive renaming (putStrLn to putStrLnCo)
  5  open import Data.String
  6  open import Function using (_∘_)
  7  
  8  putStrLn = putStrLnCo ∘ toCostring
  9  
 10  infixl 1 _>>_
 11  
 12  postulate
 13      _>>_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (IO B) → IO B
 14      getLine : IO String
 15  
 16  {-# COMPILED _>>_  (\_ _ _ _ -> (>>)) #-}
 17  {-# COMPILED getLine (getLine) #-}
 18  
 19  main : IO Hask.Unit
 20  main =
 21      putStrLn "Hello, World!" >>
 22      putStrLn "Whatup!" >>
 23      getLine >>= \up ->
 24      putStrLn ("Your face is " ++ up)

• IO.Primitive does not define >>, so we do.
• (\_ _ _ _ -> (>>)) throws away the type arguments, because Haskell does not have type arguments.
• Agda has no do notation.

The most useful Agda resources I have found

• Dependently Type Programming in Agda
• The Agda Wiki.
• Literate hyper-linked Agda Library