The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

On Sat, Jun 21, 2008 at 10:00:43AM -0400, Adam Chlipala wrote:
> Edsko de Vries wrote:
> > [different universes for:]
> >
> >   Inductive prod (A B : Type) : Type :=
> >     | pair : A -> B -> prod A B.
> >
> > [vs.]
> >
> >   Inductive prod (A : Type) (B : Type) : Type :=
> >     | pair : A -> B -> prod A B.
> >   
> 
> Wow, that is really weird. I had been assuming that these two 
> definitions would desugar to the same internal AST. At least one of them 
> had the behavior I expected. ;-)

That behavior what intended at the beginning so as to ease universe
sharing but it turned out to be a bad choice since the basic library
itself missed the point. It would be safer then to change the
semantics (if ever some user wants universe sharing, he would have to
first give a name to the shared universe).
 
On Sat, Jun 21, 2008 at 04:20:48PM -0400, Adam Chlipala wrote:
> Edsko de Vries wrote:
> > I understand that Type is not impredicative and so when we
> > say
> >
> > Inductive prod : Type -> Type -> Type :=
> >   | pair : forall A : Type, ..
> >
> > the type of A must be a "lower" Type than the Type in the result of
> > prod. However, it seems to me that the alternative definition (with A a
> > parameter to the datatype) introduces the same impredicativity "through
> > the backdoor".
> >
> > I presume that one definition introduces a paradox somewhere but the
> > other doesn't.
>
> Maybe.  I just know that the typing rules for Gallina add "<=" for
> parameters and "<" for constructor arguments.  There's probably a good
> meta-theoretical reason for it, but you probably don't need to know the
> reason to program effectively in Gallina.

Without these internal constraints on universes, one would be able to
get phi(T):T for some type T and injective phi, from which an
inconsistency can be proved, in the same way as an inconsistency is
derivable from the existence of a set of all sets (Russell's paradox),
or from the existence of an ordinal of all ordinals (Burali-Forti's
paradox). See for instance user's contribution "Paradoxes" at
http://coq.inria.fr/contribs/paradoxes.html.

Hugo Herbelin