Zulip Chat Archive

Stream: general

Topic: universe weirdness


Kevin Buzzard (Mar 24 2019 at 09:21):

I define a function twice using two different methods and the resulting definitions have slightly different types.

def with_zero (α) := option α

instance : monad with_zero := option.monad

def with_zero.map {α β : Type*} (f : α  β) : with_zero α  with_zero β := functor.map f
def with_zero.map' {α β : Type*} (f : α  β) : with_zero α  with_zero β := option.map f

#check @with_zero.map
-- with_zero.map : Π {α β : Type u_1}, (α → β) → with_zero α → with_zero β
#check @with_zero.map'
-- with_zero.map' : Π {α : Type u_1} {β : Type u_2}, (α → β) → with_zero α → with_zero β

In the map version, the universes of alpha and beta have magically become the same.

Mario Carneiro (Mar 24 2019 at 09:25):

When you use Type*, that's basically a universe metavariable Type ?u. It gets unified in the definition

Kevin Buzzard (Mar 24 2019 at 09:28):

I had never understood that before.

Mario Carneiro (Mar 24 2019 at 09:31):

if you use Type u and Type v you will get an error on the first one

Mario Carneiro (Mar 24 2019 at 09:32):

this is why Type* is not used in core, in favor of explicit universes

Mario Carneiro (Mar 24 2019 at 09:32):

It's a bit more explicit but I think being able to almost completely forget about universes is more worthwhile


Last updated: Dec 20 2023 at 11:08 UTC