‘Hello world’ in Agda¶
Below is a complete ‘hello world’ program in Agda (defined in a file
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 or run
agda --compile hello-world.agda from the command
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
importstatement, 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 acan be compiled to a standalone executable. For example:
main = run (putStrLn "Hello, World!")runs the
putStrLn "Hello, World!"and then quits the program.