## A Type Checker that knows its Monad from its Elbow

I've been hacking a bit on Foveran lately. The main new thing that I've added is the integration of the monad laws and functor laws into the definitional equality. These additions were inspired by some suggestions of Conor, and a post on Epilogue by Pierre from some time back. I've taken a different implementation approach to the one sketched in that blog post. The scheme I am using is Filinski's normalisation by evaluation for the computational lambda-calculus, with some little extensions.

### Descriptions of Indexed Functors form a (Relative) Monad

To describe (most of) its own data-types, Foveran implements the indexed descriptions (`IDesc`

) data-type from the paper The Gentle Art of Levitation. Objects of type `IDesc I`

are codes for functors from `(I -> Set)`

to `Set`

, where `I`

is a `Set`

. The `IDesc I`

type has the following constructors:

```
“IId” : I -> IDesc I
“K” : Set -> IDesc I
_“×”_ : IDesc I -> IDesc I -> IDesc I
“Sg” : (A : Set) -> (A -> IDesc I) -> IDesc I
“Pi” : (A : Set) -> (A -> IDesc I) -> IDesc I
```

The codes are all given their actual meanings by the `semI`

operator I'll talk about below. But without really thinking about what the codes mean, one can easily see that there is a natural substitution operation on `IDesc`

s, simply because an object `D : IDesc I`

is really just a tree with holes labelled with `I`

s where the `“IId”`

s are. Such a substitution operation would have type:

```
bind : (I J : Set) -> IDesc I -> (I -> IDesc J) -> IDesc J
```

This is pretty easy to implement: just recurse down the first `IDesc I`

argument until you hit an `“IId” i`

and then apply the `i`

to the provided function. If I just implement `bind`

, though, the type checker doesn't get to know that it satisfies the (relative) monad laws. (Side note: `IDesc`

itself has type `Set -> Set 1`

, so it is a relative monad).

So I've built-in the `bind`

operation into the Foveran system and given it the following syntax:

```
bind x <- D1 in D2
```

where `x`

is bound in `D2`

.

When the Foveran type checker normalises terms of type `IDesc I`

, it knows that they have one of two kinds of normal form: either they are constructed from one of the constructors above, and all the sub-`IDesc I`

s are in normal form; or they are of the form `bind x <- D1 in D2`

where `D1`

is stuck and `D2`

is in normal form. By representing all objects of type `IDesc I`

in this way, the normaliser is able to normalise terms up to the monad laws, as I'll now demonstrate.

If the normaliser is given a variable `D : IDesc I`

with no definition, or some other stuck term, then its normal form is `bind x <- D in “IId” x`

. So I automatically get the right-unit law for (relative) monads to hold definitionally in the Foveran type theory.

The internal implementation of the `bind`

operator rearranges terms to always get things into the form described above. So nested `bind`

applications get linearised:

```
bind x <- (bind y <- D1 in D2) in D3
=
bind y <- D1 in bind x <- D2 in D3
```

This implements the associativity laws of (relative) monads.

Finally `bind`

knows what to do with any of the constructors above for building up `IDesc I`

objects: it just commutes round them until it gets to an `“IId” i`

, where it performs the actual substitution:

```
bind x <- “IId” i in D
=
D[i/x]
```

where `D[i/x]`

means `D`

with `i`

substituted for `x`

. So the left-unit law for (relative) monads holds definitionally. This is less interesting though, since this law always holds even if I define `bind`

myself rather than building it into the type theory.

### The Interpretation of Descriptions...

Given a object `D`

of type `IDesc I`

and a type `X`

with a free variable `i : I`

, the interpretation of `D`

at `X`

is given by the special type former `semI[D, i. X]`

, which obeys the following rules:

```
semI[“IId” e, i. X] = X[e/i]
semI[“K” A, i. X] = A
semI[D1 “×” D2. i. X] = semI[D1, i. X] × semI[D2, i. X]
semI[“Sg” A D, i. X] = (a : A) × semI[D a, i. X]
semI[“Pi” A D, i. X] = (a : A) -> semI[D a, i. X]
```

Given the description of the normal forms of the `IDesc I`

that I described above, it would seem odd that there is no clause for `semI`

on terms constructed from `bind`

. So let us add one:

```
semI[bind x <- D1 in D2, i. X] = semI[D1, x. semI[D2, i. X]]
```

(remember that `x`

may be free in `D2`

). By integrating this law into the normaliser, I immediately get that the semantics of composed descriptions of functors is definitionally equal to the composition of the semantics of the descriptions. In short: the normaliser, and hence the definitional equality, knows that `semI`

is a (relative) monad morphism!

### ... is a Functor

I've been saying that the `IDesc`

type describes functors, but the `semI`

operator only tells you what happens on objects. I could easily define a `mapI`

function to implement an action on morphisms:

```
mapI : (I : Set) ->
(D : I -> IDesc I) ->
(X Y : I -> Set) ->
((i : I) -> X i -> Y i) ->
semI[D, i. X] -> semI[D, i. Y]
```

If I just implement this though, I am in the same position as with the `bind`

function above: the definitional equality doesn't know that the functor laws hold. So I've added the following special operator to the Foveran type theory:

```
mapI[D, i. X, i. Y, f, x]
```

where `D : IDesc I`

(the `I`

gets inferred), `X`

and `Y`

are types each with a free `I`

variable `i`

, `f : (i : I) -> X[i] -> Y[i]`

, and `x : semI[D, i. X]`

. The whole thing has type `semI[D, i. Y]`

. (There's a lot more that could be inferred here, even without full-on type reconstruction, but this is what I've implemented at the moment).

Now I have to pull several tricks to get the functor laws to hold definitionally. The main one is forcing that the only normal forms of type `semI[D, i. Y]`

*when D is stuck* are of the form

`mapI[D, i. X, i. Y, f, x]`

.So if it has a stuck term, like a variable `x`

, of type `semI[D, i. Y]`

, the normaliser always expands it to a map of the (`I`

-indexed) identity functor over `x`

:

```
x = mapI[D, i. Y, i. Y, λi y. y, x]
```

This ensures that the identity preservation law always holds definitionally, similarly to the case for the right-unit law of the relative monad `IDesc`

above.

As one might imagine, the rest of the implementation of `mapI`

proceeds by recursion on the structure of the `IDesc I`

argument, until it gets to a `bind`

, whereupon it does something special:

```
mapI[bind x <- D1 in D2, i. Y, i. Z, f
, mapI[D1, x. semI[D2 x, i. X], x. semI[D2 x, i. Y], g, z]]
=
mapI[D1, x. semI[D2 x, i. X], x. semI[D2 x, i. Z]
, λi x. mapI[D2 i, i. Y, i. Z, f, g i x]
, z]
```

Note that the last argument on the top line must have this form, by the normal forms of stuck `IDesc`

s and the normal forms of values of type `semI`

.

This rule ensures that `mapI`

both satisfies the preservation of composition, and tracks the monad morphism behaviour of `semI`

.

### Making use: Inductive Types with Strictly Positive Parameters

There's an example of the use of the extended definitional equality in the file `parameters.fv`

in the Foveran github repo. I'll give a quick overview below. Thanks to Stevan Andjelkovic for the idea.

#### Codes for Inductive Types with Parameters

The goal of the file is to give an account of inductive data types with parameters in such a way that I can define the functor laws generically (the `IDesc`

codes above cannot, alas, define inductive data-types). For example, the type of lists of some type `A`

uses the type `A`

in a particular way that ensures that I can always define a generic map operation.

So I define a new type of codes of types indexed by some set `I`

, with parameters indexed by some other set `P`

:

```
IDescP : Set -> Set -> Set 1
IDescP P I = I -> IDesc (P + I)
```

To realise these codes as actual inductive types, I must compose them with something that handles the extra `P +`

by instantiating it with the parameters:

```
IDescP:fork : (P I : Set) -> (P -> Set) -> P + I -> IDesc I
IDescP:fork P I X x =
case x with { inl p. “K” (X p); inr i. “IId” i }
```

The complete codes are built using the following definition, which uses the `bind`

operator to compose the descriptions:

```
IDescP:code : (P I : Set) -> IDescP P I -> (P -> Set) -> I -> IDesc I
IDescP:code P I D X =
λi. bind x <- D i in IDescP:fork P I X x
```

Finally, they can be turned into actual `I`

-indexed types, given the `P`

-indexed family of parameters:

```
muP : (P I : Set) -> IDescP P I -> (P -> Set) -> I -> Set
muP P I D X = µI I (IDescP:code P I D X)
```

#### Defining Generic Map

The generic map function is now defined as follows (`cata`

is the generically defined catamorphism function, derived from the built-in induction on inductive types):

```
map : (P I : Set) ->
(D : IDescP P I) ->
(X Y : P -> Set) ->
((p : P) -> X p -> Y p) ->
(i : I) -> muP P I D X i -> muP P I D Y i
map P I D X Y f =
cata I (IDescP:code P I D X)
« muP P I D Y
, λi x. construct
(mapI[D i, x. semI[IDescP:fork P I X x, i. muP P I D Y i]
, x. semI[IDescP:fork P I Y x, i. muP P I D Y i]
, λx. case x with { inl p. f p; inr i. λx. x }
, x])
»
```

This looks complicated, but this is mainly due to `mapI`

not yet inferring as many of its arguments as it could. What is important is what I haven't written. In the `λi x. construct`

... bit, the variable `x`

has type `semI[IDescP:code P I D X i, i. muP P I D Y i]`

. By the definition of `IDescP:code`

this *normalises* to `semI[D i, x. semI[IDescP:fork P I X x, i. muP P I D Y i]`

and I can easily apply `mapI`

.

If the normaliser didn't know that `semI`

was a relative monad morphism, then `x`

's type would be `semI[bind x <- D i in IDescP:fork P I X x, i. muP P I D Y i]`

and I would've had to manually decompose into the two parts, apply the `mapI`

and then recompose. By making the definitional equality stronger, I can get away with writing less code.

### What other Laws can be built-in?

What other laws can be built-in to the definitional equality? I believe that Conor wants to build the concept of free monad over a functor into Epigram, so that the monads laws automatically hold for all (for some intensionally defined version of "all") free monads. In the full-blown levitation scheme, `IDesc`

would itself just be one free monad among many, and the laws would automatically hold for it. I think the `semI`

and `mapI`

laws would have to be still added specially though.

There are also subsets of the functors described by `IDesc`

codes that have special properties. If one stays away from codes that introduce "data" (i.e. codes that describe containers with no shapes) then it is automatically an applicative functor. The `lift`

/`All`

construction used for describing generic induction is the leading example of this type. Dually, if one stays away from codes that introduce a choice of positions, one automatically get the (nameless?) dual of an applicative functor (e.g. the `Somewhere`

modality). Maybe it would be interesting to let the relevant laws hold automatically in these cases as well?