‘Hello world’ in Agda

This section contains two minimal Agda programs that can be used to test if you have installed Agda correctly: one for using Agda interactively as a proof assistant, and one for compiling Agda programs to an executable binary. For a more in-depth introduction to using Agda, see A taste of Agda or the list of tutorials.

Hello, Agda!

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

  1. data Greeting : Set where
  2.   hello : Greeting
  4. greet : Greeting
  5. greet = hello

This program defines a data type called Greeting with one constructor hello, and a function definition greet of type Greeting that returns hello.

To load the Agda file, open it in Emacs and load it by pressing C-c C-l (Ctrl+c followed by Ctrl+l). You should now see that the code is highlighted and there should be a message *All done*. If this is the case, congratulations! You have correctly installed Agda and the Agda mode for Emacs. If you also want to compile your Agda programs, continue with the next section.

Hello, World!

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

  1. module hello-world where
  3. open import Agda.Builtin.IO using (IO)
  4. open import Agda.Builtin.Unit using (⊤)
  5. open import Agda.Builtin.String using (String)
  7. postulate putStrLn : String → IO ⊤
  8. {-# FOREIGN GHC import qualified Data.Text as T #-}
  9. {-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
  11. main : IO ⊤
  12. main = putStrLn "Hello world!"

This code is self-contained and has several declarations:

  1. Imports of the ÌO, ⊤ and String types from the Agda Builtin library.

  2. A postulate of the function type putStrLn.

  3. Two pragmas that tell Agda how to compile the function putStrLn.

  4. A definition of the function main.

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. This will create a binary hello-world in the current directory that prints Hello world!. To find out more about the agda command, use agda --help.

Note

As you can see from this example, by default Agda includes only minimal library support through the Builtin modules. The Agda Standard Library provides bindings for most commonly used Haskell functions, including putStrLn. For a version of this ‘hello world’ program that uses the standard library, see Building an Executable Agda Program.