hello world for agda

Agda is an interesting new language in the style of haskell but uses a different type system that is very interesting. If you don't know about it I'm not going to help you (it's too late at night) so do a search. This blog post is to gve those already interested an example "hello world" example in agda:

module helloworld where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Data.Char using (Char)
open import Foreign.Haskell using (fromColist; Colist; Unit)
open import Data.Function
open import Data.Unit

fromString = fromColist ∘ toCostring

main : IO Unit
main = putStrLn (fromString "Hello, world!")


To compile this the commandline is: agda -i [library path] -i . -c helloworld.agda

Note that the file name must be "helloworld.agda" and [library path] must be the path to the src directory of the experimental standard library . I tested this program with standard library version 0.2 along with agda 2.2.4 as packaged in ubuntu 9.10.

The first time you try to compile will take a long time and a lot of RAM. Note the funny symbol on the fromString line. This is a unicode character and you might need to copy and paste it from the web browser (that's how I put it in my program anyway).

Hopefully copying and pasting that will just work without mangling the special character.