The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Wed, Apr 18, 2007 at 03:32:52PM +0200, Benjamin Werner wrote:
> Here is a funny example using the new form of sort polymorphism of  
> the inductive types and the new rules for parameters of V8.1.

Thanks. That was most illustrative.

Here's my quick intuition of what's going on: the sort-polymorphism is
universe polymorphism with a Haskell-like "monomorphism restriction":
_functions_ from types to types are polymorphic in the index of the
type, but a type associated with a top-level definition has a fixed
index. So in your example:

> (* the type of sets whose elements are indexed by type A *)
> Inductive ens (A:Type) : Type :=
> sup :  (A-> {B:Type & (ens B)})->(ens A).

This is polymorphic: the index of (ens foo) depends on the index of foo.

> (* A set is a set together with its carrier type *)
> Definition ENS := {A:Type & (ens A)}.

But this is monomorphic. ENS gets some fixed universe.

> (* the set of all sets, indexed by the type of sets *)
> Definition big : (ens ENS).

This is all right: big again gets a fixed universe which is
constrained to be larger than the univercse of ENS.

> (* Is this set a set ??? *)
> Definition BIG : ENS.
> exists ENS.
> exact big.
> Defined.

But this fails, since the defined object has a larger universe than ENS. 

A funny consequence of the "monomorphism restriction" is that
definitions are even less referentially transparent than before. I
have always hated how factoring a common term into a supposedly
transparent definition breaks automation and proofs since definitions
aren't automatically unfolded everywhere. But that's nothing compared
to this:

Definition ENS2 := { A : Type & ens A }.

Definition BIG2 : ENS2.
exists ENS.
exact big.
Defined.

This works without inconsistencies. ENS2 has exactly the same
definition as ENS, but since it is a different top-level variable, it
gets assigned its own universe variable. So now we still have to
construct instances for different universes separately, but at least
we can factor all the common stuff out, and this is a big improvement.

However, it means that if we want to prove theorems
universe-polymorphically, we can never ever use the names ENS or ENS2,
as those are fixed to a particular universe. Instead, we have to say
"forall (A : Type) (e : ens A), ..." everywhere, which is a bother...

Hm, wait a second, isn't { A : Type & ens A } polymorphic, too? So
perhaps the best thing would be to use a _syntactic_ definition that
expands to the above. I must try that out and see how it fares.

Still, it would be nice to be able to have truly transparent ordinary
definitions.

Thanks again for your example.


Lauri