difference between `Type*` and `Type _`?

Stream: new members

[llllvvuu]

Is there any difference between Type* and Type _? (besides Type* requires mathlib)

[Kyle Miller]

Type* creates a fresh universe level variable u and elaborates to Type u, and Type _ creates a fresh universe level metavariable ?u and elaborates to Type ?u.

[Kyle Miller]

If you have (X Y : Type*) then for example X = Y would be a type error (they have different universe level variables), but (X Y : Type _) would allow X = Y since the universe level metavariables can unify.

[Kyle Miller]

(note that (a b : ty) elaborates as (a : ty) (b : ty), with ty elaborated twice)

[llllvvuu]

Kyle Miller said:

If you have (X Y : Type*) then for example X = Y would be a type error (they have different universe level variables), but (X Y : Type _) would allow X = Y since the universe level metavariables can unify.

Thanks for the explanation!

[Julian Berman]

(This may not be true anymore, or may be controversial, so I'll say it anyway so that someone disagrees if it isn't) but I think @Eric Wieser told me to generally avoid Type _ unless you're really sure you want that behavior, because it can cause Lean to do some expensive unification (in the way Kyle mentioned).

[Matthew Ballard]

If Type* fails and Type _ is ok, then you probably have secret universe constraints floating around

[Matthew Ballard]

You will only see it for type synonyms now

[Julian Berman]

But in the case that both work, Type _ can end up being lots slower as Lean tries to find some potentially non-trivial minimal universes to satisfy all the holes right?

[Eric Wieser]

When Type* succeeds you should always use it over Type _

[Eric Wieser]

It doesn't succeed on type synonym def MyNat : Type* := Nat, where Type _ is ok.

[Eric Wieser]

Everywhere else, probably you should work out what the _ is being inferred as and write that instead

[Matthew Ballard]

Yes, generally you should be explicit about levels anyway. They get introduced automatically (autoimplicit) still and can have a dramatic effect on the performance as Lean needs to do an additional solve for each step

[Matthew Ballard]

Even though it probably yields no benefit peformance-wise, I would still try to avoid Type _ in synonyms. That way everyone who reads the code knows where everything live explicitly. This is just my opinion though

[Julian Berman]

Can you (either of you) explain what's special about type synonyms?

[Julian Berman]

Is it because Nat itself is defined using Type _?

[Matthew Ballard]

API boundaries

[Matthew Ballard]

Oh wait. Sorry. I thought you meant their use.

[Julian Berman]

Ah I see, so you're saying "use the one you find from the thing I'm aliasing"?

[Julian Berman]

No I understand what they're for yeah, just not why Type _ is then something needed

[Matthew Ballard]

Here you have a secret constraint. The level of the thing after := better be the same as the level of the synonym

[Julian Berman]

Got it, right, makes sense, thanks.

[Eric Wieser]

Matthew Ballard said:

Even though it probably yields no benefit peformance-wise, I would still try to avoid Type _ in synonyms. That way everyone who reads the code knows where everything live explicitly. This is just my opinion though

I think the argument is probably that no one really cares about the universe; but people certainly want to see def foo : Type _ := maybeAType instead of def foo := maybeAType

[Matthew Ballard]

I think that is also the reason why levels can be introduced implicitly still

[Matthew Ballard]

eg [Category C]

[Kyle Miller]

@Julian Berman Beyond performance, an additional concern with Type _ is that your theorems might be more specialized than you think.

-- "All types are subsingletons"
example (α : Sort _) (x y : α) :
    letI : Subsingleton α := inferInstance
    x = y :=
  Subsingleton.elim _ _

-- Oh, no they're not.
example (α : Sort*) (x y : α) :
    letI : Subsingleton α := inferInstance -- fails
    x = y :=
  Subsingleton.elim _ _

[Kyle Miller]

This was the primary motivation for Type*/Sort*

[Matthew Ballard]

After they got introduced, at least one thing was found to live in Type 0 for example

[Julian Berman]

And what's happening there (and I'll butcher the terminology I'm sure, sorry), is that while Lean is elaborating the actual type after the :, it's doing that before it works out the _ in the binder, and so once it gets to that it picks a narrower _ than it "should"?

[Kyle Miller]

If you change that example to a def and #print it you'll see

[Kyle Miller]

Or maybe even move your cursor right before x = y to see what instance it picked up in the local context

[Matthew Ballard]

Except I don't think there is a "should". It fills in what works without telling you what choices it makes do so

[Kyle Miller]

There's a "should" in the sense that when you write α : Sort _ you wrote it because you thought it would make it be more polymorphic than it ends up being

[Julian Berman]

Right I meant in ^ sense that I still don't really understand when this behavior is so desirable.

[Julian Berman]

It seems like a footgun.

[Kyle Miller]

Exactly, that's why we made Type*/Sort*

[Matthew Ballard]

As Eric said, the counterpoint is that is it is a pain to write

universe a b c d ... A B C ... a1 b1 c1 ...

[Kyle Miller]

The desirability of Type _ is that _ is a plain old universe level placeholder (which elaborates to a fresh plain old universe level metavariable). That is, it's just a combination of basic features.

[Kyle Miller]

and there's no mechanism in Lean to make a metavariable that isn't unifiable with a constant, or whatever the rule is supposed to be where it's not a footgun