The Coq mailing list

[Judicael Courant <Judicael.Courant AT lri.fr>]

Bruno Barras wrote :
> One interesting proposal is from Judicael Courant. He suggests that
> all universes and constraints should be explicitely stated by the user
> (and be included in modules). Maybe Judicael can comment better on this.
> 

Sure!

The aims of this proposal are:
1) Nothing should happen behind the back of the user. Otherwise, the
user gets confused, ask for features in order to know what happens and
finally gives us to much work :-)
2) It should not expect the casual user to be familiar with universes
3) It should be at least as powerfull as the current scheme

A first idea would be just to make universes be explictly given.
Then, we would have (Type 0) : (Type 1) : (Type 2) : ....
This satisfy 1), I consider 2) is ok, but 3) is not.
With the current scheme, you can let a universe float until you use it.
This is not possible if you can put only integer constants as a universe
level.

Therefore I propose to add explicit universe variable. You could
introduce a new variable, say "u", then write (Type u) in order to
denote the associated type. Then, the type of (Type u) should be (Type
u+1), the type of the latter being (Type u+2),...
I mean, the grammar for universes should be:

universe ::= integer_const
           | variable
           | universe + integer_const

and we would also need something like
           | max(universe,universe)
in order to successfully typecheck (x:Type u)(Type v)

We would then obtain something really close to the current
implementation if the typechecker just checks that there is a
assignation of integer to universe variables that satisfy the universe
constraints. This would then satisfy 2) and 3) but I am not satisfied
with 1). 

Rather, I suggest a set of constraints be explictly given by the user
and the typechecker checks that for all assignation that satisfy them,
the term being typechecked is well-typed.

Now, this could pose some problems introduce a set of constraints
that is unsatisfiable: you could prove False (you have the same problem
with Axiom here) and make non-normalizing terms typecheck (much worse!).

A solution to this problem would be to let the user only introduce
satisfiable constraints, for instance by letting him only introduce
constraint at the time he introduces a new variable: the introduction a
new variable "u" could be given together with a constraint "u>=e". Since
e would contain only previously introduced universe variables, this
would ensure that the constraints are satisfiable.

Now, as for instantiating a variable, we could introduce a construct
"Instantiate u = e". The problem there is that we have again the problem
of checking this does not make the constraints unsatifiable. Moreover, a
variable could be instantiated only once.

In fact, this system would work at its best together with modules.
Forget about such an "Instantiate" command, instantiation would be done
by Functor instantiation.

For instance, you could make a theory T of type
FunctorType(X:sig
               universe u;
               universe v>=u+2;
               universe w>=max(u+3,v);
               term A : (Type u);
              end)
  ->
   sig
    <<many things about X.u, X.v, X.w, X.A>>
   end

then, you could introduce a universe z, and apply T
to 
 struct
  universe u := z+1;
  universe v := z+3;
  universe w := z+4;
  term A := Type z;
 end

The typechecker would just check that the constraints v>=u+2,
w>=max(u+3,v) hold for the assignation above and that A is of type (Type
u).


I have thought a little bit about an algorithm for typechecking the
constraints and I hope I have one that is sound and complete. I plan to
write this down in the next few months...


Judicaël.
-- 
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Montre moi des morceaux de ton monde, et je te montrerai le mien"
Tim, matricule #929, condamné à mort.
http://rozenn.picard.free.fr/tim.html