# 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 :

## 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

Instead of

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

In general, instead of function

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

### Variable

### Application

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