universes

Stream: Program verification

[Johan Commelin]

Naive newbie question: Lean has a hierarchy of universes. Do these ever show up in software development? Or is Prop + Type all you need?

[Mario Carneiro]

It comes up in some naive higher order programming, e.g. if you want a monad transformer with a coherence property that universally quantifies over all monads

[Mario Carneiro]

I remember struggling with a definition of io that didn't bump the universe, because it existentially quantifies over a monad satisfying some interface operations

[Sebastian Ullrich]

Existentials also come up in containers of (runtime) heterogeneous elements

#check List (Σ α : Type, Σ _ : ToString α, α)  -- list of printable things

[Mario Carneiro]

If we wrote haskell code like the lens library we would have universe bumps all over the place:

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

[Mario Carneiro]

runST also has a higher order type quantification

[Sebastian Ullrich]

In practice though, for anything you ever want to stick in a monad, Type is the only viable kind :upside_down: . Because bind requires alpha and beta to be in the same universe, you have to agree on a single "monadic universe" for the whole program.

[Mario Carneiro]

I rather think that all these examples don't want more universes, but instead system F (which can be summarized as Type 1 = Type)

[Johan Commelin]

Aha, thanks for the replies!

[Kevin Buzzard]

So the conclusion is that Lean has infinitely many universes only to make its type theory consistent, and neither mathematicians nor computer scientists need anything other than Prop or Type?? Given that universes sometimes cause issues, isn't this an argument for just being much less polymorphic? :-)

[Eric Wieser]

Doesn't the problem usually manifest as trouble _writing new_ polymorphic lemmas, rather than _applying_ old ones? So there'd be no advantage to de-polymorphizing existing code.

[Eric Wieser]

Why does bind require the universe to stay the same?

[Kyle Miller]

Eric Wieser said:

Why does bind require the universe to stay the same?

Iirc, it's because a monad is a particular functor, and you can't quantify over universe variables (you can say F.{u} for a specific level u is a monad, but you can't require that F.{u} is a monad for all u.)

[Matthew Ballard]

The agitation in Rust for type constructors associated to traits is a good sign for the pratical value for devs. (Please correct me if I am confused here.)

[Mario Carneiro]

@Kevin Buzzard There is another solution, which is to not have universes at all, or only have one. You then have to deal with the fact that some types are "small" and others are "large" and the large ones don't have a type in the formal system. This is how ZFC works and IMO it's quite possible to make do with this

[Chris B]

What do you do when you want to make a statement about a large type? Are there any proof assistants that use this approach?

[Kyle Miller]

Chris B said:

What do you do when you want to make a statement about a large type? Are there any proof assistants that use this approach?

Maybe related is (at least one version of) Automath, which only had the Prop and Type type universes. What happens is that not every theorem/definition has a type -- essentially it has two classes of functions, the usual lambda abstractions (which have types), and, not sure what to call them, metafunctions (which don't).

Imagine a modification to Lean, where in place of explicit universe levels you can have other kinds of arguments:

lemma id.(α : Type) : α → α := λ x, x

The id function is too big to have a type itself in a two-universe system, but, for example, id.(ℤ) would have the type ℤ → ℤ : Type.

(One annoyance is that this id cannot be used with Props, which is something the Sort hierarchy solves in Lean.)

[Kyle Miller]

Just like how in Lean you can't have functions that take arguments that quantify over universe levels (and instead you have to specialize a given function with some specific universe levels, possibly universe variables), you can't have functions that take these metafunctions as arguments without specializing all of the metafunction arguments to specific values. (I wonder how you'd deal with monads on Type?)

[Chris B]

Thanks, I'll check automath out. The metafunction/"fixed at point of use" idea is sort of what I figured it might be.

[Mario Carneiro]

@Chris B In metamath, the distinction I am making corresponds to sets versus classes. You can prove theorems about classes, but class quantification is always implicit and always a universal closure, similar to how universe parametric definitions in lean work. (You can't prove that there exists a class satisfying such and such, but you can construct a concrete class and prove it satisfies such and such.) In a type theory, it would probably work out that large types can appear in the context, and they can be substituted but not quantified over, and the typing judgment for large types would be something like |- A type instead of A : Type because Type is not an object in this language.

[Mario Carneiro]

Kyle's example is right on the money. The distinction between regular arguments and const-generic/type arguments in Rust (and early vs late bound lifetimes) is also of a similar flavor.

[Mac]

Sebastian Ullrich said:

In practice though, for anything you ever want to stick in a monad, Type is the only viable kind :upside_down: . Because bind requires alpha and beta to be in the same universe, you have to agree on a single "monadic universe" for the whole program.

Could this just be solved with a more generalHBind? For example:

class HBind (m : Type u1 → Type v1) (n : Type u2 → Type v2) where
  hBind {α : Type u1} {β : Type u2} : m α → (α → n β) → n β

@[defaultInstance] instance [Bind m] : HBind m m := ⟨bind⟩

Such a bind would also be useful for asynchronous programming (as its signature is compatible with that of bindAsync).

[Chris B]

@Mario Carneiro

So it seems like it's along the lines of mm0's first/second order distinction, where first order would be small and second order is large. The strategy in peano.mm1 of using hand-rolled metaprograms to get ad-hoc polymorphism (ala eqtac) seems to work pretty well even in the absence of a fancier typeclass/resolution system.

In an mm1 project where there are a large number of sorts, can you use annotations to fake a {A}, List A that does monomorphization at points of use to get you List <concrete sort>, or would that blow up too quickly?

[Mario Carneiro]

You actually don't need metaprograms to get the required instantiations here; instantiation just directly works on a theorem with second order free variables (in fact, this is the preferred way to state lemmas). You would only need a metaprogram to simulate third order variables

[Mario Carneiro]

You would also need a metaprogram to get sort-polymorphism in MM0, this is not directly supported. That would be one (very much not recommended) way to implement a rich type system in the sorts, by just minting a new sort whenever you need a different type. I guess you could call that monomorphization

[Mario Carneiro]

It's not recommended though because a lot of the architecture assumes that the number of sorts is small finite (like, less than 128) so a scheme like that would quickly blow the implementation limits

[Chris B]

Boo. Thanks for humoring me.

[Mario Carneiro]

If users started pushing for that it wouldn't be that hard to increase the limit, but I'm trying to discourage that kind of use. It makes about as much sense as having thousands or tens of thousands of syntax categories

[Mario Carneiro]

Or Type 10000 for that matter

[Mac]

Mario Carneiro said:

It makes about as much sense as having thousands or tens of thousands of syntax categories

Personally, this makes a lot of sense to me. :laughing: I am actually working on something privately that made do this kind of thing.

[Mac]

The library essentially uses syntax categories as a substitute for type classes (and inductives -- so types in general).

[Chris B]

Mario Carneiro said:

If users started pushing for that it wouldn't be that hard to increase the limit, but I'm trying to discourage that kind of use. It makes about as much sense as having thousands or tens of thousands of syntax categories

This makes sense in the context of mm0 as a theorem prover prover. If you were to import something like mathlib or another large formalization from a different system, I assume you would keep their declarations as "things that are stated in terms of the sorts set out in lean.mm1".

[Mario Carneiro]

Right. Each importer might have a different set of sorts, but it is a function only of the formal system itself so it's usually actually a small number. For lean I think there are 3 sorts, for terms, levels and inductive specifications