LARA

Simple Types for Lambda Calculus

There are several type systems for lambda calculus

We consider here the simplest one

  • types are disjoint
  • only primitive and function types
  • every lambda binding specifies its type

Type Rules for Simply Typed Lambda Calculus

Environment $\Gamma$ maps variable names to types

Variable

\begin{equation*} \frac{(x \mapsto T) \in \Gamma} {\Gamma \vdash x : T} \end{equation*}

Application

\begin{equation*} \frac{\Gamma \vdash f : T_1 \to T_2,\ e : T_1} {\Gamma \vdash (f\, e) : T_2} \end{equation*}

Abstraction

\begin{equation*} \frac{\Gamma \oplus \{x \mapsto T_1\} \vdash e : T_2} {\Gamma \vdash (\lambda x:T_1.e) : T_1 \to T_2} \end{equation*}

Example Primitive Operations

Among the primitive operations we consider 

plus : int -> int -> int
ite  : bool -> int -> int

Example: Type check the lambda expression

\begin{equation*} (\lambda f : \mbox{int}\to\mbox{int}.\ \lambda x : \mbox{int}.\ f(f\ x)))\ \ (plus\ 8) \end{equation*}

in environment $\Gamma = \{ {plus} \mapsto (\mbox{int} \to \mbox{int} \to \mbox{int}), 8 \mapsto \mbox{int} \}$