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