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: if % denotes $\lambda$, type check lambda expression 

(%f:int->int. (%x:int. f(f x))) (plus 8)

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