Sort vs Type

Stream: new members

[Lars Ericson]

In Theorem Proving in Lean 4 at the end of the section on Dependent Type Theory we see

#check @id        -- {α : Type u_1} → α → α

A run of #check @id in Lean 4 Web gives, instead of {α : Type u_1} → α → α, the result

@id : {α : Sort u_1} → α → α

We can put in two versions of id and get either Type u_1 or Sort u_1:

def ident {α : Type u} (x : α) := x
#check ident        -- ident.{u} {α : Type u} (x : α) : α

def ident1 {α : Sort u} (x : α) := x
#check ident1    -- ident1.{u} {α : Sort u} (x : α) : α

SoSort u or Type u are equivalent in the above example.

My understanding is that Prop is a synonym for Sort 0 and Type is a synonym for Type 0 and Type 0 is a synonym for Sort 1 making Type n a synonym for Sort (n+1).

Does having both Sort and Type in Lean 4 add value? It seems like one or the other would be sufficient. What am I missing?

[Kyle Miller]

Type u is exactly Sort (u + 1) internally.

One reason for Type u is that Prop has some different rules for which universe a pi type lives in. If you work with Sort u sometimes the universe level expressions can get more complicated than if you just used Type u.

One reason for Sort u is that then you can make definitions that work for Prop too. Potentially Lean could just not have Sort at all, leaving you to create separate definitions for Prop and Type u. It's nice being able to define a single definition that works for both when possible.

[Lars Ericson]

Thanks for the explanation! It would be nice to write this down in a record similar to Python PEPs. The explanation shows that it is a parsimonious choice.

I'm curious why the choice of abbreviation is sticky in the interpreter in the sense that it remembers whether I used Type or Sort in

def ident {α : Type u} (x : α) := x
#check ident        -- ident.{u} {α : Type u} (x : α) : α

def ident1 {α : Sort u} (x : α) := x
#check ident1    -- ident1.{u} {α : Sort u} (x : α) : α

when under the hood they are equivalent (i.e. why doesn't this normalize to one canonical choice).

[Yakov Pechersky]

They are not equivalent. Type u will never be Prop. Sort u can be.

[Eric Wieser]

As you said yourself

Lars Ericson said:

Type n a synonym for Sort (n+1).

So of course Lean knows the difference between Type u and Sort u, because they are different

[Eric Wieser]

I suspect if you write Sort (u +1), Lean still prints it as Type u, which would a way to disprove your "stickiness" claim.

[Lars Ericson]

@Eric Wieser consider this code

def ident {α : Type u} (x : α) := x
#check ident        -- ident.{u} {α : Type u} (x : α) : α
#check ident True

def ident1 {α : Sort u} (x : α) := x
#check ident1    -- ident1.{u} {α : Sort u} (x : α) : α
#check ident1 True

This gives the following messages in Lean 4 Playground (Zulip provides a button to push on top right corner of the snippet, so you can reproduce):

LeanProject.lean:2:0
ident.{u} {α : Type u} (x : α) : α
LeanProject.lean:3:0
ident True : Prop
LeanProject.lean:6:0
ident1.{u} {α : Sort u} (x : α) : α
LeanProject.lean:7:0
ident1 True : Prop

The first version gives Type u in the signature. The second version gives Sort u in the signature. So Lean is remembering whether Type or Sort was used in the input definition. Also, ident with Type u works fine on a Prop even though "Type u will never be Prop". I wouldn't call "stickiness" a "claim". It is just an observation of the behavior of the interpreter: Sort in comes out as Sort. Type in comes out as Type. And, in this case, Prop unifies with Type.

[Junyan Xu]

def ident {α : Sort (u + 1)} (x : α) := x
#check ident        -- ident.{u} {α : Type u} (x : α) : α -- Not printed as Sort (u + 1)
#check ident True

is what Eric is telling you.
(As an aside, I've heard that Lean 4 normalizes universes aggressively.)

[Sabrina Jewson]

Clearly not that aggressively ;)

example : Sort (imax u (imax v w)) = Sort (imax (max u v) w) := rfl -- fails :(

[Lars Ericson]

OK so Sort u stays as Sort u because u could be 0 but Sort (u+1) normalizes to Type u.

I'm still confused about this:

def ident {α : Type u} (x : α) := x
#check ident True

because per above Type u should never match Prop and True is a Prop.

To verify that True is a Prop I write:

def x : Prop := True
#check x  -- gives back x : Prop
#eval x     -- throws an error

The #eval x gives error

failed to synthesize
  Decidable x

This is above my head. Why can't it just give back True?

[Henrik Böving]

I'm a bit surprised that this Type u with Prop thing works myself but regarding the eval question: Evaluation is not doing some type theoretic lambda calculus reduction stuff, it attempts to compile and (somewhat) efficiently execute your code in a VM.

If you want to do reduction in the lambda calculus style you'll have to use #reduce, note that #reduce is not expected to be very performant so if you wish to do actual computation you should prefer eval.

[Matt Diamond]

I don't see anything contradictory about this:

def ident {α : Type u} (x : α) := x
#check ident True

When you call ident, you pass in True as x. Since the type of True is Prop and you declared that the type of x is α, α equals Prop. And since the type of Prop is Type (which you can verify with #check Prop), {α : Type u} checks just fine.

[Eric Wieser]

The failing test would be #check ident trivial

[Eric Wieser]

Lars Ericson said:

OK so Sort u stays as Sort u because u could be 0 but Sort (u+1) normalizes to Type u.

There's not really any normalization going on here, it's just the pretty-printing rules

[Lars Ericson]

I understand: Prop is a synonym for Sort 0, and Sort 0 has type Sort 1 a/k/a Type 0 a/k/a Type, and

def ident {α : Type u} (x : α) := x
#check ident trivial -- Fails
#check ident -- ident.{u} {α : Type u} (x : α) : α
#check id -- id.{u} {α : Sort u} (a : α) : α
#check id trivial -- Succeeds