meta + universes

Stream: general

[Reid Barton]

Could/should :four_leaf_clover: allow meta to break "universe safety", e.g., stick a field of type Type inside a structure declared to have type Type?

[Reid Barton]

To support things like existential types in Haskell

[Sebastian Ullrich]

It's not a bad idea. We have discussed it before, but there are some issues in the details. For example, we would still like to distinguish between values and proofs in the compiler. Anyway, you should be able to define existential types in meta Lean 3 using a generalized version of unchecked_cast that can cast between universes

[Mario Carneiro]

Ah, this is a nice idea, I hadn't thought about using unchecked_cast to enable universe casting. I'll add an interface for this in mathlib

[Mario Carneiro]

I think that the best way to enable this kind of thing in meta land without having a whole different language is to do all universe checks as normal, but drop the check on maximum universe levels for meta inductives

[Mario Carneiro]

so it would still generate the same recursors as normal, but if the type is supposed to be Type 3 and you say Type 1 instead then that's okay

[Sebastian Ullrich]

Right, we discussed that before but never followed up on it https://github.com/leanprover/lean/pull/1580#issuecomment-301203751

[Mario Carneiro]

@Sebastian Ullrich Whoa, this was not expected. Not only does the advertised method not work, but I think I can prove there is no workaround, that is, VM evaluation respects universes! This means that something like universe inconsistent inductives may be the only way to make this work.

[Kenny Lau]

can we define a function that sends u : nat to Type u?

[Mario Carneiro]

u : nat does not typecheck

[Kenny Lau]

not even in the unsafe level?

[Mario Carneiro]

they are not the same thing

[Mario Carneiro]

levels and natural numbers are completely different, syntactically

[Kenny Lau]

where is max defined?

[Mario Carneiro]

nowhere, it's primitive

[Mario Carneiro]

Basically, unchecked_cast works by casting across a sorried proof of type equality, which is erased by the VM so that the equality recursor just steps directly from one type to another, and hopefully the VM representations match up so this makes sense. But the equality can only go between two elements of the same universe, and similarly with heq. Indeed, if you look at the recursor of any inductive, it has a motive that lands in Type l for some fixed l, and you can only move from one place to another along this family, meaning you can never escape Type l by application of this recursor.