The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

I agree with your remarks. However, I do not think it is the restriction
or lack of polymorphism for the constants which makes the definitions
less transparent.

If we had full universe polymorphism, we could indeed define BIG : ENS

Then we could prouve that BIG is set-theoretically an element of BIG.

But it would not be an element of "itself", because the two  
occurences of
BIG would have different universe indices (fortunately, because if they
had not, we would have Russell's paradox).

To be explicit: we could prove

th1 : IN BIG BIG

th2 : forall E : ENS, ~(IN E E)

but if we try to type

th2 BIG th1 (which should be of type False) then we would get
the universe inconsistency (indeed, at the very last step before
the paradox).

So indeed, a syntactic definition corresponds better to what is
proved.

I have only glanced very quickly through Randy and Bob's paper,
and I saw it deals with the question of delta-conversion, but I had
no time to understand what is the position wrt such examples.


 Cheers,


Benjamin


Le 18 avr. 07 à 18:48, Lauri Alanko a écrit :


> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club