## A Tale of Normalisation

In the last post we left off having gone through the basics of Dhall and defining an `Either`

type. For this post the aim of the game is to look into defining `Functor`

s in Dhall and then seeing how `Yoneda`

relates to `Functor`

s and why it helps us in Dhall. Without further ado, let's get stuck in with `Functor`

!

## Functor

To begin, let's deconstruct what we know about `Functor`

(in most programming languages) and build up the definition from there. The first thing we know about `Functor`

is that it abstacts over some `f`

that has a kind `Type β Type`

.

The other thing we know about `Functor`

is that it defines a higher-order function called `map`

. This higher order function takes an `(a β b)`

and gives us back a function `f a β f b`

.

To define this in Dhall we define it is a record type with a field called `map`

. So let's see what that looks like:

```
Ξ»(f : Type β Type)
β { map : β(a : Type) β β(b : Type) β (a β b) β f a β f b }
```

Breaking this down we can see:

- An
`f`

that is of type`Type β Type`

, corresponding to our required kind. - A record containing a field
`map`

which defines the higher-order function. - The higher-order function for all
`a`

, and for all`b`

, and the required function`(a β b) β f a β f b`

.

Placing this in a file `Functor/Type`

and running it through Dhall we get:

```
$ dhall <<< "./Functor/Type"
β(f : Type β Type) β Type
Ξ»(f : Type β Type) β { map : β(a : Type) β β(b : Type) β (a β b) β f a β f b }
```

With that I invite you to try implement `Functor`

for `Either`

under a file called `Either/functor`

. If you get stuck the solution is below. Some things to note are that you will need to import the `Either`

type that was defined in the last post (or write it in-line), and the `Functor/Type`

we have just defined to add a type annotation so that we make sure we aren't lying about the implementation.

```
let Functor = ./../Functor/Type
in let Either = ./Type
in Ξ»(a : Type)
β { map =
Ξ»(b : Type)
β Ξ»(c : Type)
β Ξ»(f : b β c)
β Ξ»(either : Either a b)
β let E = constructors (Either a c)
in merge
{ Left =
Ξ»(x : a) β E.Left x
, Right =
Ξ»(x : b) β E.Right (f x)
}
either
}
: Functor (Either a)
```

Since `Either`

has a kind `Type β Type β Type`

we have to introduce what the `a`

for the `Left`

part of the union type. Then we introduce the types we will be transforming in our `map`

function (`b`

and `c`

in this case) and the `either`

that we will be mapping over. We will need to construct new values of type `Either a c`

, handling each case of the union. Finally we collapse the `either`

we were given and reconstruct a new one with function `f`

applied to the `Right`

side.

## Traffic Problem with `merge`

This is where we're going to see that we run into a bit of code bloat with Dhall. Let's look at what happens when we `map`

multiple functions one after the other over some `Either`

value.

```
let Either = ./Either/Type Text Natural
in let map = (./Either/Functor Text).map
in Ξ»(e : Either)
β map
Natural
Natural
(Ξ»(i : Natural) β i + 5)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 4)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 3)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 2)
(map Natural Natural (Ξ»(i : Natural) β i + 1) e)
)
)
)
```

Not the prettiest code ever but it will be demonstrative of the point so let's run this through Dhall:

```
$ dhall <<< "./lots-o-map"
β(e : < Left : Text | Right : Natural >) β < Right : Natural | Left : Text >
Ξ»(e : < Left : Text | Right : Natural >)
β merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = y + 5 | Left : Text >
}
( merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = y + 4 | Left : Text >
}
( merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = y + 3 | Left : Text >
}
( merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = y + 2 | Left : Text >
}
( merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = y + 1 | Left : Text >
}
e
)
)
)
)
```

That's a lot of nested merges! And if we output it into a file by doing `dhall <<< "./lot-o-map" > output`

we can inspect the size of it and we can see it's 941B. In more complicated use cases where you are using `map`

repeatedly your expressions can become GBs; Woof! πΆ

Sure this seems like a trivial case but it can occur (and did in our Formation code base) in more complex code. While using Dhall at work we had a `traverse`

that contained multiple uses of `map`

inside the body, that traversed a large AST of nested unions. This meant there was a lot of `map`

s accumulating. We had an output of 300MB, which was slowing down the Haskell code that was trying to read this in. So what can we do about it?!

## Yo, Yoneda!

Enter `Yoneda`

! I first heard about this through my good friend reasonablypolymorphic. Sandy was talking about `Yoneda`

and how it can help Haskell generics code for more efficient implementations. On top of this, I recently saw a post by Icelandjack laying out a wonderful derivation on `Yoneda`

giving a good intuition of the underlying theory.

In this post we will see how it becomes useful in Dhall code, and we will start by seeing how we define it in Dhall.

We can define `Yoneda`

in Dhall like so:

```
Ξ»(f : Type β Type) β Ξ»(a : Type) β β(b : Type) β (a β b) β f b
```

We will make this easier to digest by looking at each part individually. The first thing we have is an `f`

that is of kind `Type β Type`

. We then have an `a`

of kind `Type`

.

When these are applied we get back a higher-order function `(a β b) β f b`

for all `b`

. This description should start to sound *very* familiar.

`Yoneda`

is known as the "Free Functor" because we can define a `Functor`

`map`

operation on it for *anything* that is of kind `Type β Type`

!

So at this point we should look at how the `Functor`

implementation is defined for `Yoneda`

:

```
-- unfortunately we have to define this here...
let compose =
Ξ»(a : Type)
β Ξ»(b : Type)
β Ξ»(c : Type)
β Ξ»(f : b β c)
β Ξ»(g : a β b)
β Ξ»(x : a)
β f (g x)
in let Yoneda = ./Type
in Ξ»(f : Type β Type)
β { map =
Ξ»(a : Type)
β Ξ»(b : Type)
β Ξ»(g : a β b)
β Ξ»(yoneda : Yoneda f a)
β Ξ»(c : Type)
β Ξ»(k : b β c)
β yoneda c (compose a b c k g)
}
: ./../Functor/Type (Yoneda f)
```

At the top we define `compose`

to make the definition a bit easier to read, and unfortunately there isn't a builtin way to compose two functions in Dhall.

Moving on, since `Yoneda`

has kind `(Type β Type) β Type β Type`

we need to introduce our `f : Type β Type`

. We then see our usual set up of `map`

but things get interesting at `Ξ»(c : Type)`

.

Remember that `β(b : Type)`

? Well the `Ξ»(c : Type)`

is fulfilling this part of `Yoneda`

for us. Next, `Ξ»(k : b β c)`

is the `(a β b)`

part of the `Yoneda`

definition. For the final line we'll inspect each piece individually because it can be a bit mind-melty π.

- Reasoning about the type of
`yoneda : Yoneda f a`

we can find that it's`β(b : Type) β (a β b) β f b`

since we have just applied the first two requirements,`f`

and`a`

. `yoneda c`

applies the`c`

type to our`β(b : Type)`

so its type is`(a β c) β f c`

`compose a b c k g`

seems a bit noisy, but the first three parameters are the types`a`

,`b`

, and`c`

.It then composes our two functions`k : b β c`

and`g : a β b`

, giving us a function of type`a β c`

.- Applying the result from 3. to the result of 2. we get an
`f c`

.

So what `Yoneda`

is doing is composing the two functions and associating them to the right. This reminds us of one of the `Functor`

laws:

```
map g . map f === map (g . f)
```

On top of this function composition is associative:

```
map h . (map g . map f)
=== (map h . map g) . map f
=== map h . map g . map f
=== map (h . g . f)
```

But of course we aren't always working in terms of `Yoneda`

. We need different semantics for different scenarios. Such as error handling with `Either`

. So for this we have two functions in the `Yoneda`

tool box to help us: `lift`

and `lower`

.

`lift`

will *lift* your `f`

into `Yoneda`

and we define it in Dhall as:

```
Ξ»(f : Type β Type)
β Ξ»(functor : ./../Functor/Type f)
β Ξ»(a : Type)
β Ξ»(fa : f a)
β Ξ»(b : Type)
β Ξ»(k : a β b)
β functor.map a b k fa
```

To summarise, we need:

- Our
`f`

that we're lifting - Its
`Functor`

implementation - The
`a`

`Type`

that we're working on in the`f`

- The
`f a`

value - And the body of the
`Yoneda`

from`Ξ»(b : Type)`

onwards, i.e.`Yoneda f a`

.

Conversely, `lower`

*lowers* the `Yoneda`

to our `f`

. Defined in Dhall as:

```
Ξ»(f : Type β Type)
β Ξ»(a : Type)
β Ξ»(yoneda : ./Type f a)
β yoneda a (Ξ»(x : a) β x)
```

It uses the identity function, `Ξ»(x : a) β x)`

, and to understand why we can once again turn to one of the `Functor`

laws that states:

```
map id === id
```

So identity acts as the "default" argument that acts as a no-op and gives us back our `f`

structure.

## Slim Fast

We've jumped through all these hoops: defined `Yoneda`

, `lift`

, and `lower`

, and now what? Well let's see what happens when we change the earlier example to use `Yoneda`

.

We first `lift`

our `Either`

data into `Yoneda`

, apply the series of `map`

s, and finally `lower`

the `Yoneda`

back to `Either`

so the interface of the function still looks the same.

```
let EitherText = ./Either/Type Text
in let Either = EitherText Natural
in let lift = ./Yoneda/lift EitherText (./Either/Functor Text)
in let lower = ./Yoneda/lower EitherText
in let map = (./Yoneda/Functor EitherText).map
in Ξ»(e : Either)
β lower
Natural
( map
Natural
Natural
(Ξ»(i : Natural) β i + 5)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 4)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 3)
( map
Natural
Natural
(Ξ»(i : Natural) β i + 2)
(map Natural Natural (Ξ»(i : Natural) β i + 1) (lift Natural e))
)
)
)
)
```

And let's run it!

```
$ dhall <<< "./less-o-map"
β(e : < Left : Text | Right : Natural >) β < Right : Natural | Left : Text >
Ξ»(e : < Left : Text | Right : Natural >)
β merge
{ Left =
Ξ»(x : Text) β < Left = x | Right : Natural >
, Right =
Ξ»(y : Natural) β < Right = ((((y + 1) + 2) + 3) + 4) + 5 | Left : Text >
}
e
```

π look at that reduction! Getting some hard numbers by outputting to a file again by doing `dhall <<< "./less-o-map" > output`

, we can see that's it 221B! That's roughly 4 times smaller! The best part about this is that reduction stays constant no matter how many maps we introduce because we will always only need one merge! π Remember that 330MB I mentioned before? It was reduced to 35MB which is roughly 10 times smaller!

One open question that I have not resolved is do we definitely *need* a `Functor`

implementation to `lift`

? I said that we can use `Yoneda`

with *any* `Type β Type`

, but we still need it to be a `Functor`

in the end. This could be useful for things like `Set`

that do not fit into the `Functor`

definition due to it reliance on `Ord`

. But at least we get some sweet normalisation fusion, and that makes me a happy programmer!

Originally published on github.com