Stream: Coq users

Topic: Set vs Type


view this post on Zulip Julin S (Aug 31 2022 at 09:04):

What's the difference between Set and Type?

I mean, I see that Set:Type and that there type universes (that's what it's called, right) like Typeᵢ:Typeᵢ₊₁.

But can Set do anything that Type can't do?

Or is Set a relic from older coq versions or something?

I was trying

Inductive nat': Type :=
| O' : nat'
| S' : nat' -> nat'.

and then upon doing

Check nat'.
(*
nat'
     : Set
*)

Though I explicitly asked for nat' to be of type Type, it turned out to be of type Set.

Why is this happening?

(This is probably which has been asked numerous time, but I couldn't find an answer.)

view this post on Zulip Guillaume Melquiond (Aug 31 2022 at 09:07):

One way to look at it is to identify Set with Type_0. For readability and performance, writing Set is better, but you lose some uniformity with respect to always writing Type.

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 09:08):

Set is Type_0
it is not strictly necessary but it's more efficient than having bunches of floating universes for things like nat
(it is also used for -impredicative-set but most people don't care about that)
very confusingly : ... -> Type (with possibly empty ... ->) for inductive types has the special meaning of "try to find the smallest universe this inductive fits in", so for instance Inductive empty : Type := . Check empty. (* empty : Prop *)

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 09:11):

if you want to force an inductive to be in Type you can use either an explicit annotation or an indirection:

(* the + means you allow for there to be more universes used, in this case there are none
   when there are some and you don't use + you get the "unbound universe" error *)
Inductive nat'@{i +} : Type@{i} :=
| O' : nat'
| S' : nat' -> nat'.

Check nat'.
(* nat' : Type *)

(* alternatively *)
Definition typ := Type.
Inductive nat' : typ :=
| O' : nat'
| S' : nat' -> nat'.

view this post on Zulip Pierre-Marie Pédrot (Aug 31 2022 at 09:22):

See also https://proofassistants.stackexchange.com/questions/1551/why-not-have-prop-set-in-coq/1552#1552 for a bit of historical background

view this post on Zulip John Wiegley (Aug 31 2022 at 17:50):

My general approach is to always use Set until I discover that moment when my development needs Type, because it's helpful to see when that happens and why.


Last updated: Jan 29 2023 at 06:02 UTC