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.

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.

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!

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:

2011-12-15 14:00: Thanks
to Andrea Vezzosi in the comments for pointing out the mistake in the
old version here. I also found a bigger mistake in the types. I think
the new version is correct.

```
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`

.

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.

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)
```

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 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?