Dependent Type Theory Section

Stream: new members

[ccn]

Hi I'm reading said section from the book "Theorem Proving in Lean", and I'm having a few questions hopefully I can get some help:

image.png

Here' I'm experimenting with universe variables but I don't get why it says u_1 instead of just u also u is representing some natural number right?

[Henrik Böving]

yes u is representing a natural number...the reason it's saying u_1 is that what you see on the right hand side does not directly correspond to what you see on the left, the right hand side (aka the infoview) is autogenerated from your file + your current position using another information provided by the compiler and it appears there is a minor cosmetic bug here in this case

[ccn]

Henrik Böving said:

yes u is representing a natural number...the reason it's saying u_1 is that what you see on the right hand side does not directly correspond to what you see on the left, the right hand side (aka the infoview) is autogenerated from your file + your current position using another information provided by the compiler and it appears there is a minor cosmetic bug here in this case

Ok, so in reality the info view should be saying alpha: Type u right?

[Henrik Böving]

Yes, I think its just a cosmetic bug, I also would expect the infoview to at least be self consistent so it will most likely use the u_1 identifier in every spot where u should appear

[ccn]

If I wrote #check λ (α β : Type*) (b : β) (x : α), x Then alpha and beta are two arbitrary types right? Now if I type #check λ (α β : Type) (b : β) (x : α), x (notice the asterisk is gone), then it makes alpha and beta both have type Type ?

[Arthur Paulino]

Yeap, and you can do things like this:

variable (χ : Type)

#check χ -- χ : Type

def foo : χ → χ := sorry

#check foo -- foo : Π (χ : Type), χ → χ

[Henrik Böving]

Yes, also note that Type* actually works in a way such that in the first case alpha and beta are in fact so arbitrary that they are not necessarily in the same type universe as evident by:

variables (α β : Type*)
#check α
#check β

[Alex J. Best]

Just to give some more context here for why Lean doesn't return the exact universe variables you wrote back at you, in the following example both a and b are in type Type u, but u is a variable here, so when they interact the type may depend on two universe variables u_1 u_2, despite the fact that they both live in Type u

universe u
constant a : Type u
constant b : Type u

#check a → b -- Type (max u_1 u_2)

[ccn]

Alex J. Best said:

Just to give some more context here for why Lean doesn't return the exact universe variables you wrote back at you, in the following example both a and b are in type Type u, but u is a variable here, so when they interact the type may depend on two universe variables u_1 u_2, despite the fact that they both live in Type u

universe u
constant a : Type u
constant b : Type u

#check a → b -- Type (max u_1 u_2)

Is a → b the same thing as f: a → b ?

[Alex J. Best]

It is the type of all possible functions from alpha to beta

[ccn]

And f: a -> b would just be one of the possible elements of that set?

[Alex J. Best]

Yeah exactly

[ccn]

I know it's not sets now though right? How could I rephrase my question I just asked in terms of type theory

[Arthur Paulino]

Maybe "one possible term of that type"

[Alex J. Best]

Right, but its not a bad mental model to start with.
You can still use the terminology elements of a type, some people say terms of a type, but elements is totally fine

[ccn]

Ok thanks for explaining that

[ccn]

I just tried out #check λ (α β γ : Type*) (g : β → γ) (f : α → β) (x : α), g (f x) in a lean file, the infoview says this:

λ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (g : β → γ) (f : α → β) (x : α), g (f x) :
  Π (α : Type u_1) (β : Type u_2) (γ : Type u_3), (β → γ) → (α → β) → α → γ

What does the part after the Π mean?

[ccn]

I think that λ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (g : β → γ) (f : α → β) (x : α), g (f x) describes a function which takes in alpha of type u_, beta of type u_2, gamma of type u_3 two functions and x, and outputs the composition

[Henrik Böving]

Have you learned what the capital pi means in general yet? If not you can keep going until you do and try to ignore it for now, it's on of the fundamental concepts of dependent type theory.

[Arthur Paulino]

Maybe this book can help you with these questions: https://homotopytypetheory.org/book/
It certainly helped me (and still does)

And you don't need to go super super deep into it. The chapter 1 is highly insightful already

[Alex J. Best]

#tpil is also a good reference here https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types

[Arthur Paulino]

These videos are very good too:

• https://www.youtube.com/watch?v=TeY5niDR8yE
  
• https://www.youtube.com/watch?v=9cR2Day-4Bk
  

[ccn]

Alex J. Best said:

#tpil is also a good reference here https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types

I'm in section 2.3 rn, I guess I'll get there soon

[ccn]

Arthur Paulino said:

These videos are very good too:

• https://www.youtube.com/watch?v=TeY5niDR8yE
• https://www.youtube.com/watch?v=9cR2Day-4Bk

checking it out

[ccn]

Ok, so I'm trying to figure out why bar doesn't work whereas foo does work:

def foo := let a := nat  in λ x : a, x + 2

def bar := (λ a, λ x : a, x + 2) nat

[ccn]

I think it has to do with the order of how things are evaluated.

Would it be correct to say that bar doesn't work because first lean looks at (λ a, λ x : a, x + 2) but that doesn't make sense because we don't know what x is? in the case for foo, I think they must "sub" the nat in before it does the type check?

[Arthur Paulino]

You'd have to be able to do

def bar' := λ a, λ x : a, x + 2
def bar := bar' nat

Notice that bar' breaks for the same reason. Maybe this way you can understand it better

[ccn]

Arthur Paulino said:

You'd have to be able to do

def bar' := λ a, λ x : a, x + 2
def bar := bar' nat

Notice that bar' breaks for the same reason. Maybe this way you can understand it better

So that one is breaking because it doesn't know what type x has right?

[ccn]

Wait nvm it doesn't know what a is

[ccn]

Ok, so I think it's a problem because it can't infer what type a should be

[Arthur Paulino]

The problem is that Lean can't just assume that addition is available for x. That is, Lean can't assure that addition is defined for type a

[Arthur Paulino]

This works:

def bar' {a : Type} [has_add a] [has_one a] := λ x : a, x + 2

#check bar' -- bar' : ?M_1 → ?M_1

def bar := bar' 3

#check bar -- bar : ℕ (Lean inferred ℕ because I applied bar' to 3)

[Arthur Paulino]

And this is a bit exotic, but is more aligned with what you tried to do:

def bar' := λ a [has_add a] [has_one a], λ x : a,
begin
  tactic.unfreeze_local_instances,
  exact x + 2
end

def bar := bar' nat

#check bar -- bar : ℕ → ℕ

[Arthur Paulino]

If someone knows how to tell lean to use _inst_1: has_add a and _inst_2: has_one a directly (without relying on tactic.unfreeze_local_instances), please let us know :pray:

[Kyle Miller]

It's still tactic mode, but the usual way is tactic#exactI

def bar' := λ a [has_add a] [has_one a], λ x : a, by exactI x + 2

def bar := bar' nat

#check bar -- bar : ℕ → ℕ

[Arthur Paulino]

Much better!

[Kyle Miller]

(I'd never looked at the definition of exactI until now. It just does tactic.unfreeze_local_instances then tactic.freeze_local_instances for you before doing exact, so it's essentially equivalent to what you'd written, but fewer keystrokes.)

[Mario Carneiro]

@ccn One thing about the original question that no one seems to have pointed out is that when you write

universe u
constant a : Type u

you are really defining a parametric family of constants, denoted a.{u}. It's not like a exists in some particular universe u, rather there is a different a at each universe: a.{0} : Type 0, a.{1} : Type 1 and so on. This is the same way that the variables command works: every definition is implicitly universally quantified over variable declarations in scope, and when you use the definition later you can supply different values for the variables.

Universe parameters are usually implicit, so when you write #check a what it really means is #check a.{_}. Lean has to pick some universe variable to fill the _, and it makes up u_1 as a universe variable name. So the output is saying a.{u_1} : Type u_1, although the .{u_1} part is hidden unless you set set_option pp.universes true.

[Yuri de Wit]

Alex J. Best said:

#tpil is also a good reference here https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types

I guess this is the relevant part?

This is an instance of a Pi type, or dependent function type. Given α : Type and β : α → Type, think of β as a family of types over α, that is, a type β a for each a : α. In that case, the type Π x : α, β x denotes the type of functions f with the property that, for each a : α, f a is an element of β a. In other words, the type of the value returned by f depends on its input.

[ccn]

Arthur Paulino said:

This works:

def bar' {a : Type} [has_add a] [has_one a] := λ x : a, x + 2

#check bar' -- bar' : ?M_1 → ?M_1

def bar := bar' 3

#check bar -- bar : ℕ (Lean inferred ℕ because I applied bar' to 3)

what does has_one mean here? Is it connected to the one in the type of it? bar' : ?M_1 → ?M_1, what do those question marks mean?

[Alex J. Best]

has_one is a typeclass, its what lets us type 1 : a and have lean know what that means, nat already has a has_one typeclass built in so you don't notice it. Given has_one and has_add lean knows what 2 and 3, etc. mean for a given type

[Alex J. Best]

The questionmarked variables are metavariables

[Arthur Paulino]

Yeah, you can read bar' : ?M_1 → ?M_1 as "bar' is a function that, given a term of a type, returns a term of that same type, whatever that type is"

And Lean differentiates "whatever types" by saying ?M_1, ?M_2...

[ccn]

Ok, so I'm trying to get this into my head, so if I have Π x : α, β this represents α → β which is the type of functions from alpha to beta.

When we have something like this: Π x : α, β x then what it saying is that this is the type of functions so where for any such function f and element a in α, then f a is an element of β a.

So if α consists of the points a_0, a_1, a_2, ... then Π x : α, β x is the type of functions α→ Union over a_i β a_i ?

[Reid Barton]

You could think of them as functions of that type such that for each input i, the output value belongs to β i

[ccn]

Reid Barton said:

You could think of them as functions of that type such that for each input i, the output value belongs to β i

So it means that the co-domain of any one of those functions has to at least contain { β i : i in α}, but could be a super set of that?

[Reid Barton]

Well, now you're mixing type theory and set theory terminology in a way that's probably making things more confusing

[Reid Barton]

A dependent function in type theory doesn't really have a codomain because the result type depends on the input value

[Reid Barton]

so maybe it is best to just avoid this language

[ccn]

Ok I will. I watched this video: https://youtu.be/TeY5niDR8yE?t=757 so is it ok to think about types as space and then the terms of a type as the points of the space?

[ccn]

This is from TPIL

Suppose we wish to write a function cons which inserts a new element at the head of a list. What type should cons have? Such a function is polymorphic: we expect the cons function for ℕ, bool, or an arbitrary type α to behave the same way. So it makes sense to take the type to be the first argument to cons, so that for any type, α, cons α is the insertion function for lists of type α. In other words, for every α, cons α is the function that takes an element a : α and a list l : list α, and returns a new list, so we have cons α a l : list α.

It is clear that cons α should have type α → list α → list α. But what type should cons have? A first guess might be Type → α → list α → list α, but, on reflection, this does not make sense: the α in this expression does not refer to anything, whereas it should refer to the argument of type Type. In other words, assuming α : Type is the first argument to the function, the type of the next two elements are α and list α. These types vary depending on the first argument, α.

Couldn't cons be of the the type Type -> type Type -> list Type -> list Type ?

[Reid Barton]

ccn said:

is it ok to think about types as space and then the terms of a type as the points of the space?

You can, although in Lean the "spaces" are more specifically discrete spaces, i.e., just sets.

[Kyle Miller]

@ccn Reid's right that there's not really a codomain, but you can transform dependent functions into non-dependent ones by creating "the" codomain using a sigma type:

def to_total {α : Type*} {β : α → Type*} (f : Π (x : α), β x) : α → (Σ (y : α), β y) :=
λ x, sigma.mk x (f x)

Using the space analogy, this sigma type is the total space of a fiber bundle, where above each y lies the fiber β y. Then the original f here "is" a section of this fiber bundle.

[Kyle Miller]

(The sigma type is basically a disjoint union.)

[Patrick Massot]

ccn said:

Ok I will. I watched this video. so is it ok to think about types as space and then the terms of a type as the points of the space?

Watching video about some foundations they are related to the foundations used by Lean but different will very likely bring you a lot of confusion.

[ccn]

variable α : Type
variable β : α → Type
variable a : α
variable b : β a

#check (a, b)            -- (a, b) : α × β a
#check sigma.mk a b      -- Σ (a : α), β a

I'm having some trouble differentiating these two objects, can anyone enlighten me?

[Kyle Miller]

@ccn

variable α : Type
variable β : α → Type
variables (a a' : α)
variable b : β a
variable b' : β a'

#check (a, b)            -- (a, b) : α × β a
#check (a', b)           -- (a', b) : α × β a
#check (sigma.mk a b : Σ (x : α), β x)      -- Σ (a : α), β a
#check (sigma.mk a' b' : Σ (x : α), β x)    -- Σ (a : α), β a
#check (sigma.mk a b' : Σ (x : α), β x)     -- error

The first are non-dependent pairs, so the second element does not depend on the value of the first. The last example shows that sigmas need the second element to have a type determined by the first element.

[Arthur Paulino]

(a, b) is another way of calling the constructor of prod, which is prod.mk:

variable α : Type
variable β : α → Type
variable a : α
variable b : β a

#check prod.mk a b       -- (a, b) : α × β a
#check sigma.mk a b      -- Σ (a : α), β a

They (prod and sigma) are different structures, you can ctrl+click on them to see their definitions

[Kyle Miller]

In principle, the non-dependent pair (the cartesian product) is a sigma type where the second argument does not depend on the first argument, in exactly the same way that the function arrow is a pi type. However, in Lean prod and sigma are actually different so this is only an analogy.

[Kyle Miller]

Products could have been defined this way:

def myprod (α : Type*) (β : Type*) : Type* := Σ (x : α), β

[ccn]

Ok, so is prod.mka dependent type too, since you can pass in a second argument which depends on the first?

[Yakov Pechersky]

prod.mk is a term, not a type

[ccn]

Should I have said the type of the term produced by prod.mk a b?

[Yaël Dillies]

prod.mk is a dependent function

[Kyle Miller]

Tada:

#check @prod.mk
/-
prod.mk : Π {α : Type u_4} {β : Type u_5}, α → β → α × β
-/

It's dependent in a very weak way (it's the kind of dependent function that Haskell 98 has, which is type polymorphism).

[Kyle Miller]

ccn said:

Should I have said the type of the term produced by prod.mk a b?

Probably not, since the type of the term produced by prod.mk a b doesn't depend on anything. (Assuming that a and b are some fixed terms.) Also, the second argument does not depend on the first -- notice that the type of prod.mk has independent types α and β for its two explicit arguments.

[Kyle Miller]

(What I was trying to point out with #check (a', b) earlier is how #check (a, b) is misleading.)

[ccn]

universe u
def ident {α : Type u} (x : α) := x

variables α β : Type u
variables (a : α) (b : β)

#check ident      -- ?M_1 → ?M_1
#check ident a    -- α
#check ident b    -- β

def ident_v2 (x : α) := x

#check ident_v2
#check ident_v2 a

Why does ident_v2 a cause this problem:

type mismatch at application
  ident_v2 a
term
  a
has type
  α : Type u
but is expected to have type
  Type ? : Type (?+1)

Shouldn't it be ok since a is of the type α?

[Reid Barton]

What was the output of #check ident_v2?

[Arthur Paulino]

The first parameter that ident_v2 expects is the type of the second parameter

#check ident_v2 α a -- ident_v2 α a : α

You can see it here:

#print ident_v2 -- def ident_v2 : Π (α : Type u), α → α := λ (α : Type u) (x : α), x

[Kyle Miller]

This should fix it:

variables {α β : Type u}

That way alpha will be an implicit argument.

[Reid Barton]

variables aren't fixed, they turn into extra arguments of definitions. In this case, the argument is explicit because of the way α was declared. So you need to pass it explicitly to use ident_v2.

[ccn]

Can anyone provide a concrete example of when a Pi type is used? I'm still having some trouble grasping it. Thanks!

[ccn]

Ok, here's an example of one:

constant modus_ponens :
  Π p q : Prop, Proof (implies p q) →  Proof p → Proof q

So would this be the type of functions f where giving the arguments p and q, then then f p q has the type Proof (implies p q) → Proof p → Proof q

Does it mean pretty much that this is a "template" where if you give two propositions, you get a proof of modeus_ponens for those specific Props p and q ?

[Kevin Buzzard]

The statement of Fermat's Last Theorem is a pi type.

[Kevin Buzzard]

Because the equation depends on the input variables

[Marcus Rossel]

ccn said:

Does it mean pretty much that this is a "template" where if you give two propositions, you get a proof of modeus_ponens for those specific Props p and q ?

I'm not sure if thinking about them as "templates" is really helpful.
The parameters p and q are just "normal" parameters, too. The only difference is that all the other parameters (after the comma) are allowed to reference p and q.
Perhaps this example motivates this better:

array is a type of fixed length arrays (like a list, but with an additional parameter in the type that constrains the size of the array):

#check array --  ℕ → Type u → Type u
#check array 10 nat -- Type u

-- for comparison:
#check list --  Type u → Type u
#check list nat -- Type u

Let's say you want to define a function that returns the last item in a given array of integers of length 10:

def array.last (a : array 10 int) : int :=
  a.read 9

Obviously it would would be nice to write this function more generically for all lengths. So we add a parameter n for the length:

def array.last (n : nat) (a : array n int) : int :=
  a.read n-1 -- this wouldn't actually work exactly like this, but for the example it's ok

This is now a dependent function, as the type of a depends on the value n.

#check array.last -- Π (n : ℕ), array n int → int

But as you can see n is still just a regular parameter. In fact, we use it in the body of the function.

[Mario Carneiro]

(it's irrelevant for the example, but you want a.read (n-1) instead of a.read n-1)