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 IDescs, simply because an object D : IDesc I is really just a tree with holes labelled with Is 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 Is 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 IDescs 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?