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:

     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:

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.

4 comments:

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

    ReplyDelete
  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:

    MAlonzo/Code/Foreign/Haskell.hs:5:18:
    Could not find module `IO.FFI'
    Use -v to see a list of the files searched for.

    ReplyDelete
  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.

    ReplyDelete
  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 goyangfc.com 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

    ReplyDelete