Making an Agda program output to the console

Question

I've been using Agda for 9 months now. For the first time, I find myself wanting to "run" (as a top-level executable) an Agda program that prints a string. Call me old-fashioned.

I can write a program that computes a string and get Agda to show me the value of the string in interactive mode (or Emacs). But the string is long and has embedded newlines. I would like it actually printed out.

By way of comparison, in GHCi I can do something like this:

Prelude> putStrLn "hello, world!"
hello, world!

But in Agda's interactive mode I get this:

Main> putStrLn "hello, world!"
.IO.♯-15
('h' .Data.Colist.Colist.∷
 .Data.Colist.♯-2 'h'
 ('e' .Data.List.List.∷
  'l' .Data.List.List.∷
  'l' .Data.List.List.∷
  'o' .Data.List.List.∷
  ',' .Data.List.List.∷
  ' ' .Data.List.List.∷
  'w' .Data.List.List.∷
  'o' .Data.List.List.∷
  'r' .Data.List.List.∷
  'l' .Data.List.List.∷
  'd' .Data.List.List.∷ '!' .Data.List.List.∷ .Data.List.List.[]))
>>
.IO.♯-16
('h' .Data.Colist.Colist.∷
 .Data.Colist.♯-2 'h'
 ('e' .Data.List.List.∷
  'l' .Data.List.List.∷
  'l' .Data.List.List.∷
  'o' .Data.List.List.∷
  ',' .Data.List.List.∷
  ' ' .Data.List.List.∷
  'w' .Data.List.List.∷
  'o' .Data.List.List.∷
  'r' .Data.List.List.∷
  'l' .Data.List.List.∷
  'd' .Data.List.List.∷ '!' .Data.List.List.∷ .Data.List.List.[]))

So, how do I take a program like the following and run it so that I observe the effects that have accumulated in the IO value?

module Temp where

   open import Data.Unit
   open import IO

   main : IO ⊤
   main = putStrLn "Hello, world!"

I notice there's a Haskell-style run function declared in Agda's IO module, but I haven't found a way to make that help.

Answer 1

The Agda IO systems has basically two layers: the lower layer (IO.Primitive) is just a proxy to the Haskell IO, the higher layer (IO) is a wrapper built on top.

The problem with IO is that it doesn't play very nicely with termination checker. So instead of having to define every funcion with {-# NON_TERMINATING #-}, you create a new (coinductive) data type that describes IO actions and focus all problems with nontermination into one single function - run.

The run function then just translates the desription of IO action given by the high-level IO type into an actual IO action (IO.Primitive) that can be run by the runtime system.

Here's how your "Hello, world!" program should look like:

open import IO

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