Hello, World! in Agda

Example for versions agda 2.2.6

Just writing strings is not a natural task for Agda, so it needs some extra installations.

This example should be saved in file “helloworld.agda”. You’ll have to install agda standard library (agda-stdlib); this was tested with agda 2.2.6 and agda-stdlib 0.3. To compile the example, use agda -i [library path] -i . -c helloworld.agda, where [library path] is a path to where you installed agda-stdlib. This compiles Agda source code into Haskell code, and then converts it into an executable. 

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

fromString = fromColist . toCostring

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