Posted by Jesper on October 4, 2022

As we all know, static type systems are great to ensure correctness of
our programs. Sadly, in industry many people are forced to work in
languages with a weak type system, such as Haskell. What should you do
in such a situation? Quit your job? Give up and despair? Perhaps, but
I have another suggestion that I’d like to explain in this post: use
our tool `agda2hs`

.

What is this `agda2hs`

, I hear you asking? Agda2hs is a tool for
producing verified and readable Haskell code by extracting it from a
(lightly annotated) Agda program. This means you can write your code
using Agda’s support for dependent types, interactive editing, and
termination checking, and from this `agda2hs`

will generate clean and
simply typed Haskell code that looks like it was written by hand. Your
boss will be amazed that all of your code is correct from the first
try, and never even suspect that you secretly proved its correctness
in Agda!

## First steps: verifying list insertion

Let’s take a look at an example of how **you** can use `agda2hs`

to
produce provably correct Haskell code. Suppose we want to insert an
element into a sorted list. That’s easy enough:

open import Haskell.Prelude insert : {{Ord a}} → a → List a → List a insert x [] = x ∷ [] insert x (y ∷ ys) = if x < y then x ∷ y ∷ ys else y ∷ insert x ys

The syntax is deliberately chosen to be very close to the
corresponding Haskell syntax, except for the swapping of `:`

and `::`

.
I am using some definitions from the
prelude
that is included with `agda2hs`

, in particular the `Ord`

type. The
double braces `{{}}`

indicate an instance
argument,
which is Agda’s way of doing type classes.

To make `agda2hs`

do its magic, there is just one more invocation
needed:

{-# COMPILE AGDA2HS insert #-}

Now, calling `agda2hs`

on this file produces the corresponding Haskell
code:

```
insert :: Ord a => a -> [a] -> [a]
= [x]
insert x [] : ys) = if x < y then x : (y : ys) else y : insert x ys insert x (y
```

So far, so Haskell. But this looks awfully complicated, how can we ever know it is correct? Prove it, of course! One property that certainly needs to hold is that when we insert an element into a list, then that element should be in the resulting list.

data _∈_ (x : a) : List a → Set where here : ∀ {ys} → x ∈ (x ∷ ys) there : ∀ {y ys} → x ∈ ys → x ∈ (y ∷ ys) insert-elem : ∀ {{_ : Ord a}} (x : a) (xs : List a) → x ∈ insert x xs insert-elem x [] = here insert-elem x (y ∷ ys) with x < y ... | True = here ... | False = there (insert-elem x ys)

Of course this isn’t enough: defining `insert x _ = x ∷ []`

satisfies
this specification. Following the ancient tradition, I leave
identifying and proving the other properties of insertion as an
exercise to the interested reader.

## Intrinsic verification with `agda2hs`

The proof above is an example of *extrinsic* verification: we first
write a simply-typed Haskell-like function and prove properties of it
after-the-fact. Another style of proof that is sometimes easier to use
is *intrinsic verification*: here we encode the properties directly in
the type of our data, so it becomes impossible to write an incorrect
function in the first place.

Avoiding the tired example of length-indexed vectors, let’s take a
look instead at the type of height-indexed trees, i.e. trees that are
indexed by the maximum length of the paths to their leaves. There are
two ways to construct a height-indexed tree: `Tip`

produces a tree of
height `0`

, while `Bin`

takes an element of type `a`

and two subtrees,
and produces a tree of height 1 + the *maximum* of the heights of the
two subtrees.

maxNat : Nat → Nat → Nat maxNat zero n = n maxNat (suc m) zero = suc m maxNat (suc m) (suc n) = suc (maxNat m n) data Tree (a : Set) : (@0 height : Nat) → Set where Tip : Tree a 0 Bin : ∀ {@0 l r} → a → Tree a l → Tree a r → Tree a (suc (maxNat l r)) {-# COMPILE AGDA2HS Tree #-}

Since Haskell tends to get confused by terms appearing at the type
level, we need some way to indicate to `agda2hs`

that we do *not* want
the second argument to `Tree`

(the `height : Nat`

) to be translated to
Haskell. To do this, `agda2hs`

makes use of the erasure
annotations
`@0`

that are built into Agda. The nice thing about these erasure
annotations is that Agda will check that you never return or pattern
match on an erased argument, so erasing them does not affect the
computational behaviour of your program. The output is a simple
Haskell implementation of binary trees:

```
data Tree a = Tip
| Bin a (Tree a) (Tree a)
```

To implement functions on indexed datatypes, it is often needed to
*transport* an element between two types when we know that their
indices are provably equal. For this we can define the function
`transport`

(sometimes also called `subst`

):

transport : (@0 p : @0 a → Set) {@0 m n : a} → @0 m ≡ n → p m → p n transport p refl t = t {-# COMPILE AGDA2HS transport #-}

That’s surely a lot of erasure annotations! In particular, the type
operator `p`

both needs to be erased itself, but also needs to accept
erased inputs `m`

and `n`

so we can erase them as well. The result is
that `transport`

is compiled to a plain identity function:

```
transport :: p -> p
= t transport t
```

Now we can implement the `mirror`

function which recursively flips the
left and right subtrees at each node.

@0 max-comm : (@0 l r : Nat) → maxNat l r ≡ maxNat r l max-comm zero zero = refl max-comm zero (suc r) = refl max-comm (suc l) zero = refl max-comm (suc l) (suc r) = cong suc (max-comm l r) mirror : ∀ {@0 h} → Tree a h → Tree a h mirror Tip = Tip mirror {a = a} (Bin {l} {r} x lt rt) = transport (Tree a) (cong suc (max-comm r l)) (Bin x (mirror rt) (mirror lt)) {-# COMPILE AGDA2HS mirror #-}

In the recursive branch of the mirror function, we need to convert a
tree of type `Tree a (suc (max r l))`

to type `Tree a (suc (max l r))`

. To do this, we `transport`

by the proof of commutativity of
`max`

. We can now tell that `mirror`

preserves the height of the tree
*by construction*, simply from its type.

Running `agda2hs`

on this function produces the following:

```
mirror :: Tree a -> Tree a
Tip = Tip
mirror Bin x lt rt) = transport (Bin x (mirror rt) (mirror lt)) mirror (
```

While this is functional, the function `transport`

still appears in
the Haskell code! GHC is probably smart enough to inline this
definition, but our boss might be able to tell that we’re not writing
this code by hand.

To avoid this problem, `agda2hs`

allows us to annotate functions as
`transparent`

if they become an identity function after erasing all
`@0`

arguments:

`{-# COMPILE AGDA2HS transport transparent #-}`

With this change, `agda2hs`

produces the code we want, and we are saved
from our boss. Phew!

```
mirror :: Tree a -> Tree a
Tip = Tip
mirror Bin x lt rt) = Bin x (mirror rt) (mirror lt) mirror (
```

## Making monads obey the law

At the moment of writing this blog post, `agda2hs`

is still in its
infancy, so it does not yet support all of Haskell’s main
features. One especially glaring omission at the moment is the lack of
support for `do`

-notation:

headMaybe : List a → Maybe a headMaybe [] = Nothing headMaybe (x ∷ xs) = Just x {-# COMPILE AGDA2HS headMaybe #-} tailMaybe : List a → Maybe (List a) tailMaybe [] = Nothing tailMaybe (x ∷ xs) = Just xs {-# COMPILE AGDA2HS tailMaybe #-} third : List a → Maybe a third xs = do ys ← tailMaybe xs zs ← tailMaybe ys z ← headMaybe zs return z {-# COMPILE AGDA2HS third #-}

While we can use `do`

notation in Agda as shown in the example above,
this is not preserved in the translation to Haskell:

```
headMaybe :: [a] -> Maybe a
= Nothing
headMaybe [] : xs) = Just x
headMaybe (x
tailMaybe :: [a] -> Maybe [a]
= Nothing
tailMaybe [] : xs) = Just xs
tailMaybe (x
third :: [a] -> Maybe a
third xs= tailMaybe xs >>=
-> tailMaybe ys >>= \ zs -> headMaybe zs >>= return \ ys
```

Still, we can already do things that would not be possible in Haskell,
e.g. prove the monad laws for each of our monads. To do this, we first
declare a typeclass `LawfulMonad`

that is parametrized by a `Monad m`

instance and has three fields, one for each of the three monad laws:

record LawfulMonad (m : Set → Set) {{iMonad : Monad m}} : Set₁ where field left-id : ∀ {a b} (x : a) (f : a → m b) → (return x >>= f) ≡ f x right-id : ∀ {a} (k : m a) → (k >>= return) ≡ k assoc : ∀ {a b c} (k : m a) → (f : a → m b) (g : b → m c) → ((k >>= f) >>= g) ≡ (k >>= (λ x → f x >>= g)) open LawfulMonad

We can then prove the monad laws for a monad by defining an instance
of this class, for example for the `Maybe`

monad:

instance _ : LawfulMonad Maybe _ = λ where .left-id x f → refl .right-id Nothing → refl .right-id (Just x) → refl .assoc Nothing f g → refl .assoc (Just x) f g → refl

Thanks to Agda’s built-in support for eta-equality on function types, proving the monad laws for the reader monad is especially straightforward:

instance _ : {r : Set} → LawfulMonad (λ a → (r → a)) _ = λ where .left-id x f → refl .right-id k → refl .assoc k f g → refl

## Coinduction, sizes, and cubical, oh my!

Working with `agda2hs`

can be quite nice since you have the full power
of Agda at your disposal for writing proofs. As an example, let’s
implement coinductive (infinite) streams, and prove fusion of
subsequent maps on streams by using Cubical
Agda!
As a warning: this is very much still an experiment, so expect some
rough edges. I’ve made a PR for improving compatibility between
`agda2hs`

and Cubical Agda,
which should be merged soon.

First, to define coinductive types in `agda2hs`

we need to import the
`Thunk`

type. This type is ‘transparent’ (i.e. not compiled to
Haskell) but it is necessary to make Agda understand that this is
really a coinductive structure, and it should do productivity checking
rather than termination checking.

open import Haskell.Prim.Thunk

We can then use the `Thunk`

type to mark constructor arguments that
should be treated ‘lazily’:

data Stream (a : Set) (@0 i : Size) : Set where _:>_ : a → Thunk (Stream a) i → Stream a i {-# COMPILE AGDA2HS Stream #-}

We make use of sized
types
to indicate the size of a stream, i.e. the depth to which the stream
has been defined. This helps Agda’s productivity checker to determine
that the functions for producing streams we will define below are
productive. Since the size is marked as erased with `@0`

, it does not
appear in the Haskell code:

`data Stream a = (:>) a (Stream a)`

Defining functions that consume a stream is easy enough:

headS : Stream a ∞ → a headS (x :> _) = x {-# COMPILE AGDA2HS headS #-}

To force evaluation of a thunk, we use the syntax `.force`

:

tailS : Stream a ∞ → Stream a ∞ tailS (_ :> xs) = xs .force {-# COMPILE AGDA2HS tailS #-}

```
headS :: Stream a -> a
:> _) = x
headS (x
tailS :: Stream a -> Stream a
:> xs) = xs tailS (_
```

To define a function that produces a stream, we need to define the
tail “lazily”. In Agda, that is done using the syntax `λ where .force → ...`

.

repeat : a → Stream a i repeat x = x :> λ where .force → repeat x {-# COMPILE AGDA2HS repeat #-}

The function is compiled as expected, and any trace of `Thunk`

and
`force`

is gone:

```
repeat :: a -> Stream a
repeat x = x :> repeat x
```

Similarly, we define a `map`

function on streams:

mapS : (a → b) → Stream a i → Stream b i mapS f (x :> xs) = (f x) :> λ where .force → mapS f (xs .force) {-# COMPILE AGDA2HS mapS #-}

```
mapS :: (a -> b) -> Stream a -> Stream b
:> xs) = f x :> mapS f xs mapS f (x
```

As an example, we can use this to implement the infinite stream of natural numbers:

nats : Stream Int i nats = 0 :> λ where .force → mapS (λ x → 1 + x) nats {-# COMPILE AGDA2HS nats #-}

Finally, let me make good on my promise and prove map fusion on
streams by using Cubical Agda. Step one: import the `PathP`

type
and define the cubical equality type `_=P_`

in terms of it:

open import Agda.Primitive.Cubical using (PathP) _=P_ : {a : Set ℓ} → (x y : a) → Set ℓ _=P_ {a = a} = PathP (λ _ → a)

Step two: ~~draw the
owl~~ prove the
fusion:

mapS-fusion : (f : a → b) (g : b → c) (s : Stream a i) → mapS {i = i} g (mapS {i = i} f s) =P mapS {i = i} (λ x → g (f x)) s mapS-fusion f g (hd :> tl) i = (g (f hd)) :> λ where .force → mapS-fusion f g (tl .force) i

If you haven’t seen Cubical Agda being used for proving bisimilarity
before, this probably looks like magic. But if it is magic, it is
magic provided by Cubical Agda, not by `agda2hs`

. The *real* magic is
the fact that `agda2hs`

does not even need to know anything about
Cubical Agda for this proof to work!

If you want to try out `agda2hs`

for yourself, you can get it from
Github. If you are keen to see more
examples and learn of the design and implementation of `agda2hs`

, you
can take a look at our recent paper at the Haskell
Symposium.
And if you have any comments or suggestions about this post, you can
always send them to me on Mastodon or via
email.