Simply Typed Lambda Calculus

Lambda calculus is a simple and powerful notation for defining functions. Among its uses are

• foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala
• basis of higher order logic

In lambda calculus, functions have no side effects

• they are mathematical functions from arguments to results
• this model is appropriate for type checking rules, because types do not change over time
• lambda calculus also supports higher-order functions

Anonymous Functions in Lambda Calculus

A function which takes its argument and increments it by 2 is given by lambda expression . The operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition, writing instead of . Here are some example expressions and their values:

Concrete syntax for :

• Isabelle theorem prover: '(% x.x+2)5' or '(\<lambda> x.x+2)5'
• ocaml: '(function x → x+2)5'
• Haskell: '(\ x → x+2)5'
• Scala ((x:int) => x+2)(5)

Lambda Expressions

Abstract syntax of untyped lambda expressions:

That is, an expression is 1) a variable, 2) a lambda expression defining a function, or 3) an application of one expression to another.

Certain predefined variables are called constants (e.g. 7, 42, 13, but also operations +, *).

Types are given by the following grammar:

There can be additional primitive types .

Currying

we have

Therefore is a function that increments its argument by

• expression is just a shorthand for

This is called currying in the honor of Haskell Curry

we can use function

Beta Reduction

The main rule of lambda calculus is beta reduction, which formalizes function application:

Here we assume capture-avoiding substitution

• we do renaming to avoid name clashes

Example:

Rules for Constants

For each constant we have appropriate rule, for example we have

and so on, for each pair of integer constants. Similarly,

we can introduce conditional constant , writing , with rules

and so on.

If we get something like

this is a run-time type error

• program would crash at run-time or produce bad result
• we introduce a type system to avoid this

Type Rules

Environment maps variable names to types

Abstraction

Example: if % denotes , type check lambda expression

(%f:int->int. (%x:int. f(f x))) ({+} 8)

in environment

Let Expressions

Expression

can be viewed as a shorthand for

because they both evaluate to

From this follows the type rule for let expressions:

Example: We can represent non-recursive method definitions using let

In this Java-like code

  int f(int x) {
return x + 3;
}
int main(int y) {
return f(f(y+5));
}

the main function can be type checked by type checking

  let f = % x:int. x+3 in
%y:int. f(f(y+5))
<code>

===== Recursive Let (letrec) Expressions =====

How to represent recursive definitions in lambda calculus?  Consider this example
<code>
int g(int x) {
return (x <= 0 ? 1 : (x+g(x-1)));
}