Wednesday, March 14, 2012

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:


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

To run this program you will need:

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


  1  module someio where
  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 (_∘_)
  8  putStrLn = putStrLnCo ∘ toCostring
 10  infixl 1 _>>_
 12  postulate
 13      _>>_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (IO B) → IO B
 14      getLine : IO String
 16  {-# COMPILED _>>_  (\_ _ _ _ -> (>>)) #-}
 17  {-# COMPILED getLine (getLine) #-}
 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.


  1. Thank you! This is what I was looking for. :)

  2. Thank you! I finally was able to compile the thing but I guess there is some kind of bug in the current experimental backend because I get this later on:

    Calling: ghc -O -o /Users/JR/Projects/Agda/Play -Werror -i/Users/JR/Projects/Agda - main-is MAlonzo.Code.Play /Users/JR/Projects/Agda/MAlonzo/Code/Play.hs --make - fwarn-incomplete-patterns -fno-warn-overlapping-patterns

    Compilation error:

    Could not find module `IO.FFI'
    Use -v to see a list of the files searched for.

  3. Harrah's casino to go public - Aljordan14 retromegabit
    Harrah's where to order air jordan 18 retro toro mens sneakers will not run a casino in the Ak-Chin area. top jordan 18 white royal blue The how can i order air jordan 18 retro red suede casino will have a gaming floor at air jordan 18 retro red suede to me Harrah's in air jordan 18 retro toro mens sneakers sale Ak-Chin Village.

  4. The casino casino hotel at Harrah's and the LINQ - Air Jordan
    The casino hotel at Harrah's and the LINQ Hotel in Las great air jordan 7 shoes Shipping Online Vegas is the most buy air jordan 10 retro beautiful place to be if you're jordan 23 retro clearance going to visit the action 출장마사지 at the