‘Hello world’ in Agda

Below is a complete ‘hello world’ program in Agda (defined in a file hello-world.agda)

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

To compile the Agda file, either open it in Emacs and press C-c C-x C-c or run agda --compile hello-world.agda from the command line.

A quick line-by-line explanation:

  • Agda programs are structured in modules. The first module in each file is the top-level module whose name matches the filename. The contents of a module are declaration such as data types and function definitions.
  • Other modules can be imported using an import statement, for example open import IO. This imports the IO module from the standard library and brings its contents into scope.
  • A module exporting a function main : IO a can be compiled to a standalone executable. For example: main = run (putStrLn "Hello, World!") runs the IO command putStrLn "Hello, World!" and then quits the program.