Dependent Arrows vs Fun (from MetaProgramming Book)

Stream: metaprogramming / tactics

[Shreyas Srinivas]

How does a dependent arrow expression differ from the lambda abstraction in Expr?

[Kyle Miller]

Do you mean docs4#Lean.Expr.forallE (pi types, i.e. dependent arrows) vs docs4#Lean.Expr.lam ?

They're very similar and there is a lot of shared metaprogramming functionality (like e.bindingName!, e.bindingDomain!, and e.bindingBody!) but they behave differently in the type theory.

[Kyle Miller]

The main difference is that Expr.lam gives a term whose type is an Expr.forallE, and Expr.forallE gives a type that is some Expr.sort.

Also, among these two only Expr.lam can participate in the LHS of an Expr.app.

[Shreyas Srinivas]

Kyle Miller said:

Do you mean docs4#Lean.Expr.forallE (pi types, i.e. dependent arrows) vs docs4#Lean.Expr.lam ?

They're very similar and there is a lot of shared metaprogramming functionality (like e.bindingName!, e.bindingDomain!, and e.bindingBody!) but they behave differently in the type theory.

Yeah. I initially guessed that this would be for product types vs lambda terms. This is also how Martin Lof Type theory presentations seem to introduce them. But then I noticed that the type signatures of docs4#Lean.Expr.forallE and docs4#Lean.Expr.lam are identical.

[Shreyas Srinivas]

And it got me wondering if they weren't interchangeable. Hence the question.

[Fabian Glöckle]

yes, because their signatures are identical also in Martin Lof dependent type theories (a Pi type needs a "type family" that is a type-valued function, not too different from a "value-valued" function)
but as explained by @Kyle Miller the semantics are different, hence they are not interchangeable

[Kyle Miller]

It's possible to define a coercion from functions to types using Expr.forallE though:

instance : CoeSort ((x : α) → Sort _) (Sort _) where
  coe f := (x : α) → f x

example (h : fun (x : Nat) => 0 < x) : False :=
  Nat.not_lt_zero _ (h 0)

[Kyle Miller]

So while they're not interchangeable, at least there's a possible conversion rule from lambdas to pis.

[Shreyas Srinivas]

I think I get that they are semantically different on an abstract level. in MLTT there is a type Type, then there are types say A and values a. So it makes sense that in the language, some elements have type Type and others have terms in A and then the identification type Id_A(a,b). So there are different sorts of terms and the sort of terms that go into an expression determine whether we are dealing with a lambda type or a dependent product type.

But in Lean this raises the following question in my mind: Let us say I have a def f (x : Bool) : Type := ... and later I have def g (x : Bool) : f x := .... Will lean interpret f as a Lam or a forallE

[Kyle Miller]

f itself is an Expr.lam

[Shreyas Srinivas]

But the type of g is \Pi (x : Bool), f x?

[Kyle Miller]

Yes

[Kyle Miller]

Something like this in full: .forallE `x (.const `Bool []) (.app (.const `f []) (.bvar 0)) .default

[Shreyas Srinivas]

So if I understand this correctly, the distinction is important for the lean typechecker to distinguish between terms that appear on the left and right of the : in a typing judgement like \Gamma \entails a : A ?

[Kyle Miller]

Yeah (with the caveat that .forallE can appear both the LHS and RHS of :), and in particular I think is so that if you have a term t you can solve for a unique T such that t : T.

[Kyle Miller]

Here's an ambiguity if you only had lambdas: if you have fun (x : Nat) => 0 < x, is its type fun (x : Nat) => Prop or Prop?

[Jannis Limperg]

The two constructs look similar because λ (x : T), u and forall (x : T), U look similar. But they have completely different typing rules: forall (x : T), U is a Sort while λ (x : T), u is a forall (x : T), U (under suitable conditions). This also means different evaluation behaviour: lambdas have a β rule (so (λ (x : T), u) v == u[x := v]) but pi types don't.

[Shreyas Srinivas]

Jannis Limperg said:

The two constructs look similar because λ (x : T), u and forall (x : T), U look similar. But they have completely different typing rules: forall (x : T), U is a Sort while λ (x : T), u is a forall (x : T), U (under suitable conditions). This also means different evaluation behaviour: lambdas have a β rule (so (λ (x : T), u) v == u[x := v]) but pi types don't.

Isn't there an elimination rule for dependent product types similar to \beta-reduction, at least in MLTT? (see : https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory#dependent_product_types)

[Shreyas Srinivas]

Although this is a rule for type judgement rather than evaluation, can't we say that this rule "evaluates" the type of f(a) to be B[a/x] from f : \Pi x : A, B x and a : A?

[Shreyas Srinivas]

Kyle Miller said:

Here's an ambiguity if you only had lambdas: if you have fun (x : Nat) => 0 < x, is its type fun (x : Nat) => Prop or Prop?

Thanks, this example helps

[Jannis Limperg]

Typing and evaluation(/reduction/defeq/operational semantics/probably other jargon) are separate judgements and separate concepts. The evaluation rule for dependent functions is the one under the heading 'Computation rules for dependent product types' and it says (with somewhat confusing notation) that we have a β law for λ. You won't find an equivalent rule for pi.

[Shreyas Srinivas]

Jannis Limperg said:

Typing and evaluation(/reduction/defeq/operational semantics/probably other jargon) are separate judgements and separate concepts. The evaluation rule for dependent functions is the one under the heading 'Computation rules for dependent product types' and it says (with somewhat confusing notation) that we have a β law for λ. You won't find an equivalent rule for pi.

Thanks. this helps. My confusion probably comes from the fact that in Lean (and CIC in general), types of terms in Sort (u) are also terms of Sort (u+1) whereas in MLTT there is a clear(easier to understand) distinction between terms of type Type and terms of type A : Type for some A and even though types can depend on terms, the distinction between type and term is clear. So the confusion is mostly "why can't I apply evaluation rules for typing judgements as well" since after all the same terms can also be types of terms at a lower Sort level. But I can see now that the rules for type judgement can differ from those of term evaluation. It helps to keep track of which side of the type judgement expressions appear on.

[Trebor Huang]

The type Sort u is a term of Sort (u+1). What are "types of Sort u"?

[Shreyas Srinivas]

Trebor Huang said:

The type Sort u is a term of Sort (u+1). What are "types of Sort u"?

I corrected it. Types of terms in Sort u

[Trebor Huang]

The type of terms in Sort u is just Sort u, right? Otherwise what would "in" mean in the sentence?

[Shreyas Srinivas]

Maybe my usage of terms is incorrect. So I'll clarify with an example (put together hastily): Let f be an inductive type defined as

inductive f where
| cons (x : Bool) : f

then f is the type of terms like f.cons true and f.cons false. But f is also a term of type Type 1. My initial question has already been answered by Jannis and Kyle (or at least I think they have been for now).

[Trebor Huang]

That is also true for Martin-Lof type theories, Bool is the type of terms like true, but Bool is also a term of type $\mathcal U_0$.

[Shreyas Srinivas]

True, but there are no further levels in the hierarchy. There is Type, which contains all terms that serve the purpose of Types like Bool, Nat etc. The type construction and elimination rules work with these types (and terms of these types, because it is dependent and all that). The evaluation rules are applied to the terms of these types. So it is easy to see that there are two distinct sets of rules, one for deducing types and one for evaluation of terms (ignoring Id_A)

[Kyle Miller]

Aside: are there any systems that have two different kinds of typing judgments? Let's say t ∈ T means that t, as a term, has type T and t : U means that t, as a type, is in universe U.

Then we could say (fun (x ∈ Nat) => x < x + 1) ∈ (fun (x ∈ Nat) => Prop) and (fun (x ∈ Nat) => Prop) : Type as well as (fun (x ∈ Nat) => x < x + 1) : Prop.

It seems to me that the lambda/pi distinction serves as a way to collapse these judgments into a single one. (And also it simplifies binders -- would there now be two different types of lambdas for quantifying with respect to ∈ or to :?)

[Mario Carneiro]

Kyle Miller said:

Aside: are there any systems that have two different kinds of typing judgments? Let's say t ∈ T means that t, as a term, has type T and t : U means that t, as a type, is in universe U.

Yes, most M-L type theories that don't have a universe hierarchy have separate judgments for $\Gamma \vdash t : T$ ("$t$ has type $T$") and $\Gamma\vdash T\ {\bf type}$ ("$T$ is a type"). You can also stick a universe index on the latter. The advantage of this form is that not all types have to have types and hence it is okay if you only have 1 or 2 universes instead of an infinite hierarchy

[Mario Carneiro]

The original MLTT also makes a distinction between terms and types, and has a coercion function you could think of as CoeSort to allow terms to appear on the right side of a typing judgment. So universes are not really types containing types but rather types containing codes for types, i.e. $\Gamma\vdash A : U\implies \Gamma\vdash T(A)\ {\bf type}$

[Reid Barton]

Even type theories that do have universes are most often presented on paper with separate type and term-of-type judgments. (It is an important distinction for the categorical semantics, e.g. a context Γ is interpreted as an object $\Gamma$ of a category, a type A in context Γ is interpreted as a "display map" $A \to \Gamma$, a term t : A in context Γ is interpreted as a section $t : \Gamma \to A$ of the display map. There is also the universe $\mathcal{U} \times \Gamma \to \Gamma$, and a section of this is a different sort of thing than a display map $A \to \Gamma$.)