# Zulip Chat Archive

## Stream: new members

### Topic: dependent function types

#### Patrick Thomas (Mar 12 2019 at 04:33):

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 (Mar 12 2019 at 04:38):

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 (Mar 12 2019 at 04:39):

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 (Mar 12 2019 at 04:41):

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`

then`x : A`

makes sense, but if `3 : ℕ`

then `x : 3`

doesn't make sense

#### Patrick Thomas (Mar 12 2019 at 04:44):

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 (Mar 12 2019 at 04:47):

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

#### Patrick Thomas (Mar 12 2019 at 05:05):

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

#### Kevin Buzzard (Mar 12 2019 at 10:46):

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 (Mar 12 2019 at 16:12):

I think the key part that I was not sure about was that `X`

can be `Type`

. Thank you.

#### Patrick Thomas (Mar 13 2019 at 04:42):

"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 (Mar 13 2019 at 04:43):

yes

#### Patrick Thomas (Mar 13 2019 at 04:43):

Cool. Thank you.

#### Mario Carneiro (Mar 13 2019 at 04:45):

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 (Mar 13 2019 at 04:47):

Yes. I think that makes sense.

#### Patrick Thomas (Mar 13 2019 at 04:51):

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

#### Patrick Thomas (Mar 13 2019 at 04:52):

Isn't it a true or false proposition?

#### Patrick Thomas (Mar 13 2019 at 04:53):

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

#### Mario Carneiro (Mar 13 2019 at 05:49):

@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 (Mar 13 2019 at 06:27):

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.

Last updated: May 06 2021 at 22:13 UTC