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