# Some Useful Agda

I’ve been using Agda for a few months now. I’ve always meant to figure out how it handles IO but never have.

Today I decided to change that! So off I went to the related Agda wiki page. So hello world in Agda apparently looks like this

The first time I tried running this I got an error about an `IO.FFI`

, if you get this you need to go into your standard library and run `cabal install`

in the `ffi`

folder.

Now, on to what this actually does. Like Haskell, Agda has an `IO`

monad. In fact, near as I can tell this isn’t a coincidence at all, Agda’s primitive IO seems to be a direct call to Haskell’s IO.

Unlike Haskell, Agda has two IO monads, a “raw” primitive one and a higher level pure one found in `IO.agda`

. What few docs there are make it clear that you are not intended to write the “primitive IO”.

Instead, one writes in this higher level `IO`

monad and then uses a function called `run`

which converts everything to the primitive IO.

So one might ask: what exactly is this strange `IO`

monad and how does it actually provide `return`

and `>>=`

? Well the docs don’t actually seem to exist so poking about the source reveals

```
data IO {a} (A : Set a) : Set (suc a) where
lift : (m : Prim.IO A) → IO A
return : (x : A) → IO A
_>>=_ : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
_>>_ : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A
```

Wow.. I don’t know about you, but this was a bit different than I was expecting.

So this actually just forms a syntax tree! There’s something quite special about this tree though, those ∞ annotations mean that it’s a “coinductive” tree. So we can construct infinite `IO`

tree. Otherwise it’s just a normal tree.

Right below that in the source is the definition of `run`

```
{-# NO_TERMINATION_CHECK #-}
run : ∀ {a} {A : Set a} → IO A → Prim.IO A
run (lift m) = m
run (return x) = Prim.return x
run (m >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)
```

So here’s where the evilness comes in! We can loop forever transforming our `IO`

into a `Prim.IO`

.

Now I had never used Agda’s coinductive features before and if you haven’t either than they’re not terribly complicated.

`∞`

is a prefix operator that stands for a “coinductive computation” which is roughly a thunk. `♯`

is a prefix operator that delays a computation and `♭`

forces it.

There are reasonably complex rules that govern what qualifies as a “safe” way to force things. Guarded recursion seems to always work though. So we can write something like

```
open import Coinduction
open import Data.Unit
data Cothingy (A : Set) : Set where
conil : Cothingy A
coCons : A → ∞ (Cothingy A) → Cothingy A
lotsa-units : Cothingy ⊤
lotsa-units = coCons tt (♯ lotsa-units)
```

Now using ♯ we can actually construct programs with infinite output.

This when run will output “Hi” forever. This is actually quite pleasant when you think about it! You can view you’re resulting computation as a normal, first class data structure and then reify it to actual computations with `run`

.

So with all of this figured out, I wanted to write a simple program in Agda just to make sure that I got it all.

## FizzBuzz

I decided to write the fizz-buzz program. For those unfamiliar, the specification of the program is

For each of the numbers 0 to 100, if the number is divisible by 3 print fizz, if it’s divisible by 5 print buzz, if it’s divisible by both print fizzbuzz. Otherwise just print the number.

This program is pretty straightforward. First, the laundry list of imports

```
module fizzbuzz where
import Data.Nat as N
import Data.Nat.DivMod as N
import Data.Nat.Show as N
import Data.Bool as B
import Data.Fin as F
import Data.Unit as U
import Data.String as S
open import Data.Product using (_,_ ; _×_)
open import IO
open import Coinduction
open import Relation.Nullary
open import Function
```

This seems to be the downside of finely grained modules.. Tons and tons of imports.

Now we need a function which takes to ℕs and returns true if the first mod the second is zero.

```
congruent : N.ℕ → N.ℕ → B.Bool
congruent n N.zero = B.false
congruent n (N.suc m) with N._≟_ 0 $ F.toℕ (N._mod_ n (N.suc m) {U.tt})
... | yes _ = B.true
... | no _ = B.false
```

Now from here we can combine this into the actual worker for the program

```
_and_ : {A B : Set} → A → B → A × B
_and_ = _,_
fizzbuzz : N.ℕ → S.String
fizzbuzz N.zero = "fizzbuzz"
fizzbuzz n with congruent n 3 and congruent n 5
... | B.true , B.true = "fizzbuzz"
... | B.true , B.false = "fizz"
... | B.false , B.true = "buzz"
... | B.false , B.false = N.show n
```

Now all that’s left is the `IO`

glue

```
worker : N.ℕ → IO U.⊤
worker N.zero = putStrLn $ fizzbuzz N.zero
worker (N.suc n) = ♯ worker n >> ♯ putStrLn (fizzbuzz $ N.suc n)
main = run $ worker 100
```

There. A somewhat real, IO based program written in Agda. It only took me 8 months to figure out how to write it :)

comments powered by Disqus