dependent function types

Stream: new members

[Patrick Thomas]

Hi,

I am trying to understand the description of dependent function types as given in Section 2.8 of Theorem Proving in Lean. I think I follow up to the end of this paragraph:

"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, α."

My next guess for the type of cons might be something like λ α : Type, α → list α → list α. Is this what is being done, but with Π instead of λ? The next paragraph seems to make it more complicated than that:

"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."

Can I just set α to Type to get what I expected from this? Is this essentially what has been done in the code block later on:

universe u

constant list   : Type u → Type u

constant cons   : Π α : Type u, α → list α → list α

As an aside, why does list have the type that is given here?

If I replace Type with ℕ in the quoted paragraph then I get:

"Given α : ℕ 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."

This seems to be hinting at what might be needed for the type of functions operating on lists of arbitrary lengths, if β : ℕ → <a type involving list ℕ>?

In summary, why is the description of Π types more complicated than I expected? Is it something along the lines of the example of lists of an arbitrary length?

[Mario Carneiro]

My next guess for the type of cons might be something like λ α : Type, α → list α → list α. Is this what is being done, but with Π instead of λ? The next paragraph seems to make it more complicated than that:

It's a good guess, but the problem is that λ α : Type, α → list α → list α is not a type. It is a function that takes a type and returns a type. That is, (λ α : Type, α → list α → list α) : Type -> Type

[Mario Carneiro]

So this function acts something like list, which also has this same type (let's ignore universes for now). You can't write x : list because list is not a type. x : list A makes sense if A is a type

[Mario Carneiro]

If I replace Type with ℕ in the quoted paragraph then I get:

"Given α : ℕ 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."

Your replacement was inconsistent. You replaced α with ℕ in most places, not Type with ℕ. Generally you can't treat Type and ℕ the same because Type is a universe and ℕ is not. That is, the elements of Type have elements but the elements of nat don't. If A : Type thenx : A makes sense, but if 3 : ℕ then x : 3 doesn't make sense

[Patrick Thomas]

Oops. I think I meant:
"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."

[Patrick Thomas]

I guess my question is then, why is the type of a dependent function not Π x : Type, β x?

[Patrick Thomas]

That is, why is β not a function from types to types.

[Kevin Buzzard]

The difference between lambda and Pi is that lambda is used to construct the terms, and Pi is used to construct the types. For example X\to Y is a type, and \lam x, f x is a term of that type, if f is a function from X to Y.

The type of a dependent function is Pi x : X, f x where X can be any type, and f is a function which takes terms of type X and spits out anything. Sure X can be Type. Do you have any questions still?

[Patrick Thomas]

I think the key part that I was not sure about was that X can be Type. Thank you.

[Patrick Thomas]

"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".

Does "is an element of" in this sentence mean "has the type"? That is, "In that case, the type Π x : α, β x denotes the type of functions f with the property that, for each a : α, f a has the type β a"?

[Mario Carneiro]

yes

[Patrick Thomas]

Cool. Thank you.

[Mario Carneiro]

technically, "having the type" is not a proposition, it's just a thing that is true when you have this construction. That is, if f : Π x : α, β x and a : α then f a : β a.

[Patrick Thomas]

Yes. I think that makes sense.

[Patrick Thomas]

Wait. Maybe I am missing something. Why is "has the type" not a proposition, like "the car is red"?

[Patrick Thomas]

Isn't it a true or false proposition?

[Patrick Thomas]

Anyway, I think your second sentence makes sense to me.

[Mario Carneiro]

@Patrick Thomas In the metatheory, you can talk about "having a type" like a proposition; you can say "x is not well typed" the same as "T is not provable" and other such assertions. But in the logic itself, the basic judgment is an element having a certain type; you can only prove such assertions by chaining together other judgments. If you formalize is_red my_car : Prop, then you can prove pf : is_red my_car or pf : ¬ is_red my_car, because it's a proposition. If you have my_car : car, then this is not a thing you can negate, it's just the kind of thing that my_car is. You can't really prove facts about this, you just ask lean "what type is my_car" and it says "it's a car" and that's it. So typing judgements are not "true or false", they are "true or you can't write them down".

[Patrick Thomas]

That makes sense. I was assuming we were talking solely in the metatheory. That is, that the sentence I quoted was a proposition in the metatheory.