Stream: Coq users

Topic: Set vs Type

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.)

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.

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 *)

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'.

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

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: Apr 20 2024 at 10:02 UTC