The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

Thanks Gaëtan for your effort and your patience with my questions.

However the situation remains somehow unsatisfactory. By reading and 
rereading the documentation I cannot find a clear rule which states what is 
allowed and what is not allowed with respect to universes. As opposed to 
that, the positivity condition is stated very clearly and to my surprise, the 
justification of the positivity rule is explained with some examples which 
are short and to the point.

My intuitive explanation with the “hiding” of a higher universe type within a 
lower universe inductive definition might be correct. But it is not very 
precise and does not give a justification. Furthermore the example of the 
existential quantification does give a constraint on the universes without 
explaining the general rule.

Sorry for me insisting on this topic. Maybe it cannot be resolved easily.

Anyhow thanks for your efforts.

Helmut


> On 17 Nov 2022, at 11:12, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> 
> wrote:
> 
> >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
>>>>>