Type Environment

type-theory

Definition

Type Environment

A type environment is a finite partial map that assigns types or type schemes to variables.

Formally, for variables $x\in \mathcal{V}$ and type schemes $\sigma \in \Sigma$,

$$\Gamma :\mathcal{V}\rightharpoonup \Sigma .$$

A typing judgement $\Gamma ⊢e:\tau$ is interpreted relative to the assumptions stored in $\Gamma$.