Type Inference

type-theory

Definition

Type Inference

Type inference is the process of deriving a typing judgement for an expression without requiring all types to be written explicitly.

Formally, given a type environment $\Gamma$ and an expression $e$, type inference tries to compute a type $\tau$ such that

$$\Gamma ⊢e:\tau .$$

In systems with principal types, type inference aims to compute the most general such $\tau$.