# 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)));
}