Recently, I've been playing around with Lean, a proof assistant (and technically a programming language) that got a lot of publicity in the past year from a few mathematicians like Kevin Buzzard and Sébastien Gouëzel.
In Lean, there are lots of definitions that treat Props and Types uniformly (that is, the definition takes an argument whose type is Sort l for an arbitrary l), but there are places where something can only be a Prop, and places where something can only be a Type. And in those cases, there are often two parallel definitions which do essentially the same thing, except that one is for Props and one is for Types. So what's different between the cases where we can have a uniform definition for both, and the cases where we need two separate definitions?
In this post, I want to give a small concrete example of a case where Props and Types don't behave the same in Lean. You can follow along using this link to all the code in this post in the Lean playground if you want.
One of the few fundamental differences between Props and Types is that we have proof irrelevance for Props. Concretely, this shows up in Lean as the following theorem, which is available from the core library:
#check @proof_irrel
-- proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂
This theorem says that, given a proposition a and two proofs h₁ and h₂ of a, the two proofs are always equal in the eyes of Lean.
This might seem innocuous, but let's combine it with another theorem from the core library:
#check @congr_arg
-- congr_arg : ∀ {α : Sort u_1} {β : Sort u_2} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
This theorem (which is uniform between Props and Types, because its parameters are Sorts), says that when we apply a function f to equal arguments (a₁ and a₂, in this case), the results are equal. This is a totally reasonable theorem. If it wasn't true, f would not be a well-defined function.
But together, these two theorems say that whenever we have a function from a Prop to a Type, that function has to be a constant function. The result can't depend on the structure of the proof that we feed to the function. It can only depend on the existence of a proof, and it must always be the same result.
The confusing thing is that when we have a function from a Prop to another Prop, we are allowed to pattern-match on the structure of the input proof, so it looks like the function's result can depend on the details of the proof. But as long as we produce a proof of the target Prop in all code branches of the function, the result is always equal, by proof irrelevance! So the function is still a constant function, even though it doesn't look like one.
Ok, I said I would give a concrete example, but so far it's been pretty theoretical.
Let's say we want to talk about a world with flowers in it. And in this world, the defining characteristic of a flower is its name, so we might write the following type definition to capture it:
inductive flower : Type
| grow : forall (name : string), flower
There's just one constructor for flowers, flower.grow, which takes an arbitrary string for the name of the flower, and returns the corresponding flower.
We also want to talk about whether this is a pretty world, and let's say it's pretty iff there exists a flower. We can capture this property by having a constructor with the same type signature as the constructor for flowers:
inductive pretty : Prop
| grow : forall (name : string), pretty
Apart from having a different type name (flower vs pretty), the only difference is that flower is a Type, and pretty is a Prop. We could justify this by saying that flower is a noun, a thing that the world can have, whereas pretty is an adjective, a thing that the world can be.
Let's prove that there exist two different flowers:
def rose : flower := flower.grow "rose"
def violet : flower := flower.grow "violet"
theorem not_equal_strings : "rose" ≠ "violet" :=
dec_trivial
theorem not_equal_flowers : rose ≠ violet :=
not_equal_strings ∘ flower.grow.inj
On the other hand, any two proofs that the world is pretty are equal. Lean believes that roses and violets are pretty in exactly the same way:
def pretty_rose : pretty := pretty.grow "rose"
def pretty_violet : pretty := pretty.grow "violet"
theorem equal_proofs : pretty_rose = pretty_violet :=
proof_irrel _ _
So, we can easily write a function from the Type to the Prop:
def forget_difference : flower → pretty
| (flower.grow name) := pretty.grow name
But Lean will complain if we try to go in the other direction:
def cant_remember_difference : pretty → flower
| (pretty.grow name) := flower.grow name
-- error: recursor 'pretty.dcases_on' can only eliminate into Prop
Does this mean that the world of Props is a black hole and that we can never escape back into the world of Types? No! There are a few allowed ways to write a function which takes a proof of a Prop and returns a value of a Type, such as:
false.elim will let us provide a proof of unreachability instead of writing actual code for that branch, even if the function is supposed to return a value of a Type.
As an example of the first point, we could write the following function, which is totally fine:
def pick_one : pretty → flower :=
fun _, flower.grow "thistle"
This function just ignores the pretty flower that we give it, and instead gives us back a pretty thistle, always. Another workaround is to turn flower into a Prop, by using nonempty:
#print nonempty
/-
@[class]
inductive nonempty : Sort u → Prop
constructors:
nonempty.intro : ∀ {α : Sort u}, α → nonempty α
-/
This turns any Type α into the proposition that "there exists a value of type α". So, we can write the following function, which doesn't completely ignore the pretty flower we give it:
def look_at_this_one : pretty → (nonempty flower)
| (pretty.grow name) := nonempty.intro (flower.grow name)
In effect, wrapping a Type in nonempty gives us a version of the Type where we promise to not actually depend on the value, only on its existence, and the rest of the type system enforces that promise. Once we make that promise, we're allowed to depend on the structure of the input proof.
So, concretely, how does the type system enforce the promise that we can only depend on the structure of a proof when we're producing a proof of a Prop? To answer this, we have to look at the fundamental, low-level building blocks that Lean provides for us when we write an inductive definition. For the example above, we can see that Lean automatically defines a whole bunch of stuff just from the definitions of flower and pretty:
#print prefix flower
/-
flower : Type
flower.cases_on : Π {C : flower → Sort l} (n : flower), (Π (name : string), C (flower.grow name)) → C n
flower.grow : string → flower
flower.grow.inj : ∀ {name name_1 : string}, flower.grow name = flower.grow name_1 → name = name_1
flower.grow.inj_arrow : Π {name name_1 : string}, flower.grow name = flower.grow name_1 → Π ⦃P : Sort l⦄, (name = name_1 → P) → P
flower.grow.inj_eq : ∀ {name name_1 : string}, flower.grow name = flower.grow name_1 = (name = name_1)
flower.grow.sizeof_spec : ∀ (name : string), flower.sizeof (flower.grow name) = 1 + sizeof name
flower.has_sizeof_inst : has_sizeof flower
flower.no_confusion : Π {P : Sort l} {v1 v2 : flower}, v1 = v2 → flower.no_confusion_type P v1 v2
flower.no_confusion_type : Sort l → flower → flower → Sort l
flower.rec : Π {C : flower → Sort l}, (Π (name : string), C (flower.grow name)) → Π (n : flower), C n
flower.rec_on : Π {C : flower → Sort l} (n : flower), (Π (name : string), C (flower.grow name)) → C n
flower.sizeof : flower → ℕ
-/
#print prefix pretty
/-
pretty : Prop
pretty.cases_on : ∀ {C : Prop}, pretty → (string → C) → C
pretty.dcases_on : ∀ {C : pretty → Prop} (n : pretty), (∀ (name : string), C _) → C n
pretty.drec : ∀ {C : pretty → Prop}, (∀ (name : string), C _) → ∀ (n : pretty), C n
pretty.drec_on : ∀ {C : pretty → Prop} (n : pretty), (∀ (name : string), C _) → C n
pretty.grow : string → pretty
pretty.rec : ∀ {C : Prop}, (string → C) → pretty → C
pretty.rec_on : ∀ {C : Prop}, pretty → (string → C) → C
-/
In both cases, Lean generates lots of stuff, but it all boils down to just three things, and everything else is defined from these three things:
flower and pretty), so that we can write function signatures using the new type.
flower.grow and pretty.grow), so that we can produce values of the new type.
flower.rec and pretty.rec), so that we can write functions which consume a value of the new type and whose result depends on the internals of the value. This is where the difference between Props and Types happens.
The type signatures for the eliminators look a bit weird, so let's break them down, starting with pretty.rec because it's simpler:
pretty.rec : ∀ {C : Prop}, (string → C) → pretty → C
(pretty → C), that is, a function from proofs of prettiness to values of some target type C.
(string → C), that is, it's a function from names of pretty flowers to values of the target type C. The whole information content of a proof of prettiness is the name of a pretty flower (that is, the argument to the constructor pretty.grow), so that's what we have to work with to produce a value of the target type C. If we had more constructors for pretty, the eliminator pretty.rec would have more parameters like this, which take the arguments of a constructor and produce a value of the target type C. Each one of these parameters is like a callback that knows how to handle values produced by a particular constructor. And if we have callbacks for all possible constructors, the eliminator just dispatches to the appropriate callback.
{C : Prop}, a target type for the function that pretty.rec returns. And sure enough, this is forced to be a Prop, not a Type nor an unrestricted Sort.
For example, we could use pretty.rec to try (and fail) again to write the "obvious" function pretty → flower:
def cant_remember : pretty → flower :=
@pretty.rec
flower -- The target type
(fun name, flower.grow name) -- The callback for `pretty.grow`
-- error: type mismatch
It doesn't look like it, but the eliminator flower.rec follows the same pattern:
flower.rec : Π {C : flower → Sort l}, (Π (name : string), C (flower.grow name)) → Π (n : flower), C n
{C : flower → Sort l}, a family of target types for the function that flower.rec returns. That's because Lean uses dependent types, so each flower value can have its own target type. Also, the target types are in Sort l, so they can be Props or Types.
(Π (name : string), C (flower.grow name)), so it's a callback that uses the argument (name : string) of the flower.grow constructor, and produces a value of the target type (C (flower.grow name)) for that specific flower.
(Π (n : flower), C n), that is, a function that takes a flower n and returns a value of the target type (C n) for that flower.
For example, we can try (and succeed) to use flower.rec to write the obvious function flower → pretty:
def can_forget : flower → pretty :=
@flower.rec
(fun _, pretty) -- The target type is `pretty` for all flowers
(fun name, pretty.grow name) -- The callback for `flower.grow`