‘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 exampleopen 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 theIO
commandputStrLn "Hello, World!"
and then quits the program.