Mutually recursive definitions of datatypes - Typer

29 Oct 2016


      Hi follow Typers (or should I say Typerers)?
I bumped into a problem with the current Typer design and am looking for
ideas to solve it.
As you may know, datatypes (aka inductive types) are defined as
*expressions* of the form
inductive_ (<dummylabel> <args>) <constrs>...
such as
inductive_ (option (a: Type)) none (some a)
but the <dummylabel> is just that (a label), not a variable.
Same for the constructor names, they're just labels and not variables.
So we usually bind this to a variable in a declaration, as in:
Option = inductive_ (option (a: Type)) (none) (some a);
and constructors have the form (inductive-cons <type> <label>), which
again is just an anonymous expression which we then bind to a variable
in declarations such as
None = inductive-cons option none;
    Some = inductive-cons option some;
This is very close to the usual "paper" definition of CIC and seems to
work OK so far (tho we'll want to systematize those names, and Typer
will have to work a bit harder at trying to hide those internal
definitions so that it uses the "Option" and "Some" variables rather
than their corresponding values in error messages).
But I have a problem with mutual recursion.   Typer allows mutual
recursion in declarations via "forward type declarations".  E.g.
Nat : Type;
    Nat = inductive_ nat z (s Nat);
The way mutual recursion works is that we first collect the types of all
the mutual declarations (to build a new type environment), then type
each declaration within this new environment.  But this environment
knows nothing about the *values* of those new variables.  So if we do:
Nat : Type;
    Z : Nat;
    Nat = inductive_ nat z (s Nat);
    Z = inductive-cons Nat z;
Typer complains that it can't verify that the Nat argument to
inductive-cons is indeed an inductive type (since all it knows is that
Nat has type "Type" but it doesn't know its definition (yet)) and as
a consequence it can't figure out the type of "Z".
Of course, we can say "don't do that", and just force the user to move
the constructor declarations to after the mutual recursion, but it's
very problematic in practice.  E.g. Typically, a type declaration
will really use the "type" macro, so you write
type Option a
       | None
       | Some a;
which expands to
Option = inductive_ (Option (a: Type)) (None) (Some a);
    None = inductive-cons option None;
    Some = inductive-cons option Some;
So of course, two mutually recursive type declarations will look like
Ta : Type;
    Tb : Type;
    type Ta | Ca1 Tb | Ca2;
    type Tb | Cb1 Ta | Cb2;
which expands to
Ta : Type;
    Tb : Type;
    Ta = inductive_ Ta (Ca1 Tb) Ca2;
    Ca1 = inductive-cons Ta Ca1;
    Ca2 = inductive-cons Ta Ca2;
    Tb = inductive_ Tb (Cb1 Ta) Ca2;
    Cb1 = inductive-cons Ta Cb1;
    Cb2 = inductive-cons Ta Cb2;
At this point, you can see that it's difficult for the programmer (both
the one using the "type" macro and the one defining it) to make sure the
declarations occur after the mutual recursion.
The best idea I had so far is to change the way mutual-recursion is
handled such that the typing is each definition is not done in a context
where we only know the type of other defs, but one where we also know
the definition of all *previous* definitions.
That might prove a bit tricky to code because of how we currently handle
cases like
A : Ta;
    B : Tb;
    B = DefB;
    A = DefA;
where definitions don't come in the same order as declarations (so we
want to type-check DefB before DefA even though A will come first in
the environment since the relative ordering depends on the order of the
type declarations).
Stefan