The Coq mailing list

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

Hi,

This is related to sort-polymorphism of inductive types (chapter 4 of
the reference manual). In the type given to inductive types, "Type"
does not strictly denote a sort with formal name "Type", but any sort
which behaves like Type behaves, namely the smallest predicative
universe of the hierarchy

  proof-irrelevant Prop <= predicative Set <= Type(1) <=

in which the inductive type can be interpreted (*).

That sort-polymorphism covers Prop and Set is convenient in some
contexts, where one might e.g. overload the notation "(A * B)%type" to
also mean "A /\ B" when A and B are in Prop.

However, this overloading of the meaning of "Type" is clearly not
intuitive enough considering the number of times the question is
raised. It happens that it also creates some complications for
extraction which has to dynamically compute when a sort-polymorphic
type is finally in Prop or not. So, maybe it might be wise at some
time to think at amending Coq on this issue.

On the practical side however, beyond the fact that it is surprising,
I'm not aware of technical drawbacks of having the given type to land
in Set, as predicative Set can be thought as a Type(0). I'm waiting
for more information from Jan-Oliver to understand the situations
where landing in Prop creates problems.

Matthieu would correct me if I'm wrong but I suspect that the
following workaround would work in practice if you really wish your
type to formally be at a universe level strictly higher than Set:

Universe i.
Record R (P: nat -> Prop) : Type@{i} := {f: nat -> nat}.

Best,

Hugo

(*) Up to the fact that, internally, the Type hierarchy is not
numerical but an acyclic graph of Type universes.

On Fri, Jan 27, 2017 at 04:19:38PM -0800, Vadim Zaliva wrote:
> I do not understand why when I define a Record in sort "Type" it ends up in
> "Set"?
> 
> Welcome to Coq 8.6 (January 2017)
> 
> Coq < Record R (P: nat -> Prop) : Type :=  {f: nat -> nat}.
> R is defined
> f is defined
> 
> Coq < Check R.
> R
>      : (nat -> Prop) -> Set
> 
> Vadim
> 
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
>