The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

>Unfortunately I have not found the rule that every argument of a constructor 
must be at a smaller or equal universe to the output universe

I can't find it either although it's mentioned, eg

>One can remark that there is a constraint between the sort of the arity of 
the inductive type and the sort of the type of its constructors which will 
always be satisfied for the impredicative sorts SProp and Prop but may fail to 
define inductive type on sort Set and generate constraints between universes for 
inductive types in the Type hierarchy.

Probably a doc bug.

The reason for the rule is basically what you said earlier

>I suspect that if it were well typed, then I could ‘hide’ an object from the 
universe ‘u+1’ in the list which resides in the universe ‘u’.

which leads to inconsistency. See also 
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.Hurkens.html and 
mentioned references.

Gaëtan Gilbert

On 17/11/2022 10:45, Helmut Brandl wrote:
> > On 16 Nov 2022, at 23:35, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net 
> > <mailto:gaetan.gilbert AT skyskimmer.net>> wrote:
> >
> > The rules for inductives 
> > https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions
> >  
> > <https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions>
> > basically every argument of a constructor must be at a smaller or equal 
> > universe to the output universe of the inductive. The first argument of cons 
> > fails this.
>
> Thanks for the explanation. I have tried to read the description in the link. 
> Unfortunately I have not found the rule that every argument of a constructor 
> must be at a smaller or equal universe to the output universe. Could you 
> point to the specific paragraph which states that rule. Since the rules are 
> very technical I might have overlooked it.
>
> My intention is to understand not only the “what” of the rules, but also the 
> “why” of the rules. What is the justification of such a rule? E.g. first I 
> didn’t understand the necessity of the positivity rule of the constructor 
> types. Then I have found an example which makes the necessity of the 
> positivity rule clear. If the following inductive type were allowed
>
>     Inductive T: Type :=
>     | co: (T -> T) -> T.
>
>
> I could define a fixpoint with infinite recursion
>
>     Fixpoint run (t: T): T :=
>        match t with
>        | co f => run (f (co f))
>        end.
>
>
> Is there a similar justification for the rule you have mentioned? Does the 
> rule inhibit an inconsistency like infinite recursion?
>
> — Helmut
>
>
> > Gaëtan Gilbert
> >
> > On 16/11/2022 22:32, Helmut Brandl wrote:
> > > > On 16 Nov 2022, at 22:06, Helmut Brandl <helmut.brandl AT gmx.net 
> > > > <mailto:helmut.brandl AT gmx.net> <mailto:helmut.brandl AT gmx.net 
> > > > <mailto:helmut.brandl AT gmx.net>>> wrote:
> > > >
> > > >
> > > >
> > > > > On 16 Nov 2022, at 21:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net 
> > > > > <mailto:gaetan.gilbert AT skyskimmer.net> <mailto:gaetan.gilbert AT skyskimmer.net 
> > > > > <mailto:gaetan.gilbert AT skyskimmer.net>>> wrote:
> > > > >
> > > > >
> > > > > > I.e. the argument type of a function type can live in a higher universe than 
> > > > > > the result type.
> > > > >
> > > > > Yes, but "lst" is an _inhabitant_ of the function type, it's not the function 
> > > > > type itself.
> > > > >
> > > > > Similarly "(fun A:Type@{u+1} => A) : Type@{u+1} -> Type@{u}" is rejected
> > > >
> > > > In that case the rejection is clear to me. The term ‘A’ has type 
> > > > ’Type@{u+1}’. Therefore the function returns a result of type ’Type@{u+1}’ 
> > > > and not ’Type@{u}’ as required by the type annotation. I.e. the function on 
> > > > the left hand side of the colon is not an inhabitant of the type on the right 
> > > > hand side of the colon. The compiler must reject it.
> > > >
> > > > Are you saying that the type ’Type@{u+1} -> Type@{u}’ is not allowed to be 
> > > > inhabited? Is there such a typing rule? If there is such a typing rule, I would 
> > > > like to understand why it is there. Does the violation of such a typing rule 
> > > > create any inconsistencies like an inhabitant of the type ‘forall A: Type, A’?
> > > According to coq the type ’Type@{u+1} -> Type@{u}’ can have inhabitants. E.g. 
> > > the following is accepted by coq:
> > >    Check (fun A: Type@{u+1} => nat): Type@{u+1} -> Type@{u}.
> > > However my construction of the inductive type ‘lst’ which is an inhabitant of 
> > > exactly that type is rejected. Why is it possible to construct a function of 
> > > that type but not an inductive definition?
> > > > — Helmut
> > > >
> > > >
> > > > > On 16/11/2022 21:02, Helmut Brandl wrote:
> > > > > > I’d like to understand universes and universe polymorphism better. Therefore 
> > > > > > I have some questions:
> > > > > > The following term is well typed in coq:
> > > > > >   Universe u.
> > > > > >   Check forall A:Type@{u+1}, Type@{u}.
> > > > > > I.e. the argument type of a function type can live in a higher universe than 
> > > > > > the result type. If I try the same with an inductive type, I get an error.
> > > > > >   Inductive lst (A: Type@{u+1}): Type@{u} :=
> > > > > >   | nil: lst A
> > > > > >   | cons: A -> lst A -> lst A.
> > > > > >   *Error:*Universe inconsistency. Cannot enforce u = max(Set, u+1).
> > > > > > What is the theoretical background of this consistency error. The type of 
> > > > > > ‘lst’ is exactly the type I have checked above as well typed. I suspect that 
> > > > > > if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ 
> > > > > > in the list which resides in the universe ‘u’. Can anybody help to give a 
> > > > > > more precise explanation.
> > > > > > Regards
> > > > > > Helmut