Typed lambda calculus

reddit this

In memory of Sanjeev Kumar Aggarwal (ska).

Update: An implementation of propositional logic in agada is available on my github repository sample-code/agda/Logic.agda

In this post, I briefly introduce typed lambda calculus in its simplest form and explain the type inference rules. The Curry-Howard isomorphism appears for the first time here, although only for propositional logic.

What are types ?

We fix a set 𝒯𝒯 of base types that can be thought of as the built-in types of the language. For this post, the set of types are all terms generated inductively as follows:

τ≔t∈𝒯|τ1→τ2. τ ≔ t ∈ 𝒯 | τ_1 → τ_2.

The above inductive definition means that a type is either a basic type tt, i.e. an element of the set 𝒯𝒯, or it is the function type τ1→τ2τ_1 → τ_2 where τ1τ_1 and τ2τ_2 are themselves types. The type τ1→τ2τ_1 → τ_2 captures the type of functions whose domain is of type τ1τ_1 and range is of type τ2τ_2. There are few points that we want to clarify right away.

  1. Consider the set of propositional logic formulas where the base set of propositions is 𝒯𝒯 and the only logical connective is the logical implies ⇒⇒. There is a one-to-one correspondence with types of our language: interpret the functional type symbol →→ as the implication operator ⇒⇒. We will see in this post that this connection is not just skin deep.

  2. The types in our language are defined independent of the terms in our lambda calculus. While this is possible for the version of typed λλ-calculus that we define here, when we want more powerful types this will no more be possible. We will have to define the values and types together.

What is a well typed expression ?

Intuitively, a typed lambda calculus is a version of lambda calculus where each expression is assigned a type. This type is used to ensure that function application is of the correct type, i.e. whenever an expression ff of type σσ is applied on another expression ee of type ττ, the type σσ should be a function type τ→τ′τ → τ′, for type τ′τ′. This requires us to assign types to lambda calculus terms in a systematic way. We use the notation e:τe:τ to assert that the expression ee has type ττ. Recall that a λλ-calculus term is a variable, or an application or a λλ-abstraction. Therefore, we need to give systematic rules for assigning types for these three cases.

The base case would be to assign types to variables in an expression. We ensure that the λλ-abstraction also have to assert the type of the variable it quantifies. Thus, any λλ-abstraction is of the form λx:τ.eλ x:τ. e and the bound variables xx gets its type from this abstractions, i.e. every free occurrence of xx in ee is assumed to be having the type ττ. For the free variables, the only way we can have types is by type assumptions, a set of assertions of the kind x:τx : τ. The type of an expression thus depends on the type of the free variables in it. Therefore, a well typed lambda calculus expression should be a combination of an expression and a set of type assumption for the free variables in it. Furthermore, they should satisfy some additional rules which we call the type inference rules.

A well typed λλ-calculus expression is an ordered pair of (1) a type assumption ΓΓ together with (2) a typed λλ-calculus term e:τe:τ, written in the logical style Γ⊢e:τΓ ⊢ e:τ, subject to the following inference rules:

Variable Rule (VAR) : Γ∪{x:τ}⊢x:τ. \frac{}{Γ \cup \{ x : τ\} ⊢ x : τ}.

Rule for application (APP) : Γ⊢f:τ1→τ2;Γ⊢e:τ1Γ⊢fe:τ2. \frac{Γ ⊢ f : τ_1 → τ_2;\;\; Γ ⊢ e : τ_1}{ Γ ⊢ f e : τ_2}.

Rule for λλ-abstraction (ABS) : Γ∪{x:τ1}⊢e:τ2Γ⊢(λx:τ1.e):τ1→τ2. \frac{Γ \cup \{x : τ_1\} ⊢ e : τ_2}{Γ ⊢ (λ x : τ_1 . e) : τ_1 → τ_2}.

The notation that we used for defining well typed terms is like a set of logical deduction rules. The stuff on the top of the horizontal line are pre-conditions, i.e. stuff which we already have derived, and the stuff in the bottom are consequences. i.e. stuff that can be concluded given the pre-conditions on the top. Let us now interpret each of these rules informally:

VAR : This rule states that with no pre-conditions we can derive the type assertion x:τx: τ provided it is already an assumption. This rule takes care of the free variables in the expression.

APP : This is the rules that makes sure that the functions are applied to the right arguments. It makes sure of two things (1) We are allowed to form the expression fef e under the type assumption ΓΓ if and only if ff and ee have types τ1→τ2τ_1 → τ_2 and τ1τ_1 respectively under the assumption ΓΓ and (2) then the resulting expression fef e has type τ2τ_2 under ΓΓ.

ABS : This rules assign types to the bound variables. This rule needs a bit of getting used to as we normally think in the other direction, i.e. in the expression λx:τ1.eλ x : τ_1 . e, the occurrence of xx in ee has type τ1τ_1.

In all the above rules, we assume that the type assumptions that arise on the left hand side of the ⊢⊢ symbol satisfies some obvious conditions like, no variables should have two distinct type assumptions etc.

Curry-Howard isomorphism.

Recall that any type ττ can be seen as a proposition over the set of basic proportion 𝒯𝒯 by interpreting the function type operator →→ as the Boolean implies operator ⇒⇒. Consider the three type inference rules that we discussed and replace any type assumption x:σx : σ or type assertion e:τe : τ in the rules above with just the associated proposition σσ and ττ respectively. This gives a set of inference rules for a restricted form of propositional logic that has implies operator ⇒⇒ as the only Boolean operator. This isomorphism between type inference and logical inference rules is often called the Curry-Howard isomorphism and is one of the main ideas of type theory. The goal in the rest of the post is to give a different interpretation of typed lambda calculus so that some magic is removed out of this isomorphism.

Consider the type assertion e:τe:τ. Normally, we think of types as a subset of allowed values and the assertion e:τe:τ as saying that ee is a value in the set associated with ττ. There is an alternate interpretation which makes the logical connection easy to make. Think of ττ as a logical statement, proposition in this case. An assertion of the form e:τe: τ is thought of as ee being the proof of the statement ττ. Alternatively, we think of the type ττ as the set of all proofs of the proposition associated with ττ in which case our usual interpretation means that e:τe:τ means that ee is a proof of the proposition ττ. In this interpretation, a proof of the proposition τ1→τ2τ_1 → τ_2 should be treated a method to convert proofs of τ1τ_1 to proofs of τ2τ_2. This then gives a valid interpretation of all the rules of type inference as rules of building proofs.

VAR : We can create a proof xx of ττ if we have such a proof by one of the assumption.

APP : If ff is a proof of τ1→τ2τ_1 → τ_2 then it is a function that converts proofs of τ1τ_1 to τ2τ_2. If in addition, we have a proof ee of τ1τ_1, we can apply ff to it and get the proof fef e of τ2τ_2.

ABS : If assuming a proof xx of τ1τ_1 we were able to get a proof ee (which can make use of xx as an axiom) of τ2τ_2 then the function λx:τ1.eλ x: τ_1 . e is a proof of τ1→τ2τ_1 → τ_2 as it takes any input proof pp of τ1τ_1 and produces as output the proof e[x:=p]e[x := p] of τ2τ_2. Here e[x:=p]e[x := p] denotes replacing all free occurrence of xx by pp.

This essentially is the crux of the “types as proofs” view point. If we want to effectively use this logical content of type theory, we need to look at richer and richer types and that is what we would be doing. We make some modest enriching in this post and leave the rest for future posts.

Introduction/Elimination rules.

For the logical operator →→, the ABS rule serves as the introduction rule as its post-condition is an implication. Any proof of a formula that is essentially an implication therefore would have ABS as its last step. On the other hand APP serves the dual purpose. It is the elimination rule for the operator →→. You may think of VAR rules as both an introduction as well as an elimination rule (it introduces nothing and eliminates nothing). This style of presentation of logical rules is due to Gentzen and plays an important role in designing type theoretic systems. The introduction rules gives ways to “construct” objects of a given type and elimination rules gives ways to “use” the objects in expressions. All other operators that we introduce here will also have introduction and elimination rules.

The operators ∨∨ and ∧∧.

We would like our logic to have the conjunctions and disjunctions. At the type level we just need to add two additional type formation operators ∧∧ and ∨∨. As a result our types are now inductively defined as:

τ≔t∈𝒯|τ1→τ2|τ1∧τ2|τ1∨τ2. τ ≔ t ∈ 𝒯 | τ_1 → τ_2 | τ_1 ∧ τ_2 | τ_1 ∨ τ_2.

To prove conjunctions and disjunctions, we need ways to create values (remember they are our proofs) of type τ1∧τ2τ_1 ∧ τ_2 and τ1∨τ2τ_1 ∨ τ_2 respectively. For conjunctions, we introduce the primitive (.,.)(.,.) that pairs up two expressions to give a new expression. A value of type τ1∨τ2τ_1 ∨ τ_2 can be created in two ways: by applying the constructor 𝐢𝐧𝐥\mathbf{inl} on a value of type τ1τ_1 or by applying the constructor 𝐢𝐧𝐫\mathbf{inr} on a value of type τ2τ_2. These give the required introduction rules for the logical operators ∧∧ and ∨∨:

DISJ : Γ⊢e:τ1Γ⊢𝐢𝐧𝐥e:τ1∨τ2, \frac{Γ ⊢ e : τ_1}{Γ ⊢ \mathbf{inl}\; e \;: τ_1 ∨ τ_2}, Γ⊢e:τ2Γ⊢𝐢𝐧𝐫e:τ1∨τ2. \frac{Γ ⊢ e : τ_2}{Γ ⊢ \mathbf{inr} \;e \;: τ_1 ∨ τ_2}.

CONJ : Γ⊢e1:τ1;Γ⊢e2:τ2Γ⊢(e1,e2):τ1∧τ2. \frac{Γ ⊢ e_1 : τ_1;\; Γ ⊢ e_2 : τ_2} {Γ ⊢ (e_1,e_2) : τ_1 ∧ τ_2}.

The justification of these rules from a proof theoretic point of view is that one can give a proof of τ1∧τ2τ_1 ∧ τ_2 by giving a pair of proofs where the first component is a proof of τ1τ_1 and the second a proof of τ2τ_2. Similarly, we give a proof of τ1∨τ2τ_1 ∨ τ_2 by giving either a proof of τ1τ_1 or τ2τ_2 except that we need to explicitly state which is the case by using the appropriate constructor 𝐢𝐧𝐥\mathbf{inl} or 𝐢𝐧𝐫\mathbf{inr}.

Next we give the elimination rule for ∧∧. The corresponding language primitive that we need is the projection operators which we add as built in functions in our calculus.

PROJ : Γ⊢e:τ1∧τ2Γ⊢𝐟𝐬𝐭e:τ1, \frac{Γ ⊢ e : τ_1 ∧ τ_2}{Γ ⊢ \mathbf{fst}\; e \; :\; τ_1}, Γ⊢e:τ1∧τ2Γ⊢𝐬𝐧𝐝e:τ2. \frac{Γ ⊢ e : τ_1 ∧ τ_2}{Γ ⊢ \mathbf{snd}\;e \;:\; τ_2}.

Similarly, to obtain the elimination rules for ∨∨, we add the function 𝐞𝐢𝐭𝐡𝐞𝐫\mathbf{either} that does case by case analysis.

CASE : Γ⊢e:τ1∨τ2;Γ⊢l:τ1→τ;Γ⊢r:τ2→τΓ⊢𝐞𝐢𝐭𝐡𝐞𝐫lre:τ. \frac{Γ ⊢ e : τ_1 ∨ τ_2;\;Γ ⊢ l : τ_1 → τ;\; Γ ⊢ r : τ_2 → τ} {Γ ⊢ \mathbf{either}\;l\;r\;e\;:τ}.

We define the the type σ↔τσ ↔ τ of logical equivalence of ττ and σσ as (σ→τ)∧(τ→σ)(σ → τ) ∧ (τ → σ).

Truth, falsity and negation.

We have a proof theoretic view of truth and falsity in this setting. Propositions are “true” if they can be proved by giving a λλ-calculus expression of that type and not true otherwise. In that sense, we only have “truths” and “not truths” and every inhabited types, i.e. types for which we can construct an element with that type, is true. Explicit truth and falsity can be achieved by adding types ⊤⊤ and ⊥⊥ to the basic types 𝒯𝒯 and to make ⊤⊤ provable, we enrich the λλ-calculus with a single constant 𝐨𝐛𝐯𝐢𝐨𝐮𝐬\mathbf{obvious} of type ⊤⊤. That there is no constants with type ⊥⊥ is deliberate design choice as we do not want to prove ⊥⊥ in our logic. Once we have the type ⊥⊥, we can define the negation ¬τ¬ τ of ττ to be the type τ→⊥τ → ⊥.

The law of excluded middle, LEM for short, is the statement τ↔¬¬ττ ↔ ¬ ¬ τ and is not a basic axiom of our logic. We can in fact prove one direction τ→¬¬ττ → ¬ ¬ τ: Consider the function λxf.fxλ x f . f x. It is easy to see that we can assign to it the type τ→(τ→σ)→στ → (τ → σ) → σ for any types σσ and ττ. In particular, if σσ is the type ⊥⊥, we have τ→¬¬ττ → ¬¬τ. The converse however is not provable. This might be considered as a weakness of the logic because LEM is used through out mathematics. However, there is a distinct advantage here.

  1. The proofs that we build are constructive and

  2. If we are in dire need of the opium called LEM, we can recover it by adding a constant 𝐥𝐞𝐦\mathbf{lem} of type τ↔¬¬ττ ↔ ¬¬ τ the way we added the constant 𝐨𝐛𝐯𝐢𝐨𝐮𝐬\mathbf{obvious}. However, this is never done in practice when using a proof assistant like coq or agda

Comparison to untyped λλ-calculus.

For any typed λλ-calculus term Γ⊢e:τΓ ⊢ e : τ we can get an untyped λλ-calculus term, denoted by ee itself, by ``erasing’’ out all types from abstractions. Is it possible to do the other way? Can we assign types to an untyped λλ-calculus expression in a way that is consistent to the rules defined above? Doing this algorithmically is the type inference problem. For example, consider the expression λx.xλ x . x. Intuition tells us that this can be assigned any type τ→ττ → τ as it is the identity function. Indeed this is the case:

  1. {x:τ}⊢x:τ\{x : τ\} ⊢ x : τ by VAR

  2. ⊢(λx:τ.x):τ→τ⊢ (λ x : τ . x) : τ → τ by ABS and (1).

It turns out that not all terms can be consistently typed, for example λx.xxλ x . xx cannot be assigned any type (why?).

Recall that the computational content of untyped λλ-calculus is captured in the notion of ββ-reduction. To avoid variable collision we also need αα-conversions. It is easy to see that notion of αα-conversion and ββ-reduction can be defined in a straight forward way for typed λλ-calculus. What then is the difference? The typed version of ββ-reduction is strongly normalising. It turns out that term like Ω=(λx.xx)(λx.xx)Ω= (λx . xx) (λx .xx) and fixed point combinators cannot be consistently typed. As a result general recursion, and hence infinite loops, are not possible in this calculus.

Consistency and recursion

The Curry-Howard isomorphism gives us a way to define logical system out of typed lambda calculus. Enriching the basic typed lambda calculus with constants like 𝐨𝐛𝐯𝐢𝐨𝐮𝐬\mathbf{obvious} or 𝐥𝐞𝐦\mathbf{lem} is like adding axioms to the logical system assoicated with the language. In any logical system, we need to worry about consistency. In classical logic, a set of axioms together with the inference rules form an inconsistent system if one can prove a statement ττ and its negation ¬τ¬τ. This definition is not very useful in the type theoretic setting as it is crucially dependent on negation which we want to avoid as much as possible. An alternate way to define inconsistency is to define inconsistent system as those which proves all statements. It is this definition of inconsistency that is easier to work with in the type theoretic framework. We say that a type theoretic system, i.e. the under lying typed λλ-calculus and its type inference rules, is inconsistent if every type in inhabited. This makes sense because an inhabitant of a type ττ is the proof of the statement (associated) to ττ. In this section, we want to connect consistency and the ability to do recursion. In fact, arbitrary recursion, or equivalently a uniform way to compute fixed points, is dangerous from a consistency perspective.

We saw that the typed λλ-calculus that we defined does not support fixed point combinators and therefore does not support recursion. This severely limits the kind of programs that one can write in such a language. However, we do know that fixed points can be implemented on a computer. Can we enrich the λλ-calculus to include a fixed point combinator by force? After all, we do know how to compile it into machine code. What would happen if we just enrich the calculus with a constant 𝐟𝐢𝐱\mathbf{fix}, much like the way we included a constant 𝐨𝐛𝐯𝐢𝐨𝐮𝐬\mathbf{obvious} or 𝐥𝐞𝐦\mathbf{lem}. For this to workout, we would need to augment our type inference rules with the following rule for 𝐟𝐢𝐱\mathbf{fix}

FIX : Γ⊢f:τ→τΓ⊢𝐟𝐢𝐱f:τ. \frac{Γ ⊢ f : τ → τ} {Γ ⊢ \mathbf{fix}\;f\;:\; τ}.

This would mean that, if we some how create a function of type f:τ→τf:τ→τ then we can prove ττ using the proof 𝐟𝐢𝐱f\mathbf{fix}\; f. Recall that, for any type ττ, the typed lambda calculus expression I=λx:τ.xI = λ x : τ . x has type τ→ττ → τ. Taking its fixed point 𝐟𝐢𝐱I\mathbf{fix}\; I will give an inhabitant of ττ. Therefore, adding arbitrary fixed points will make the logic inconsistent.

Real world programming languages like Haskell does not care about this issue as writing infinite loops are too important for a programmer. In fact, every type in Haskell has an inhabitant, namely undefined. What this means is that the type system of Haskell is not directly suitable as a theorem prover although we can still use it to catch many bugs at compile time.

Languages like agda which has to double up as a proof assistant allow certain restricted kinds of recursion by making sure that the recursion is well formed. Other than the motivation to write real world programs, some restricted form of recursion is actually necessary to capture mathematical objects like natural numbers etc. We leave these issues for future posts.