> For the complete documentation index, see [llms.txt](https://isubasinghe.gitbook.io/isithas-wiki/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://isubasinghe.gitbook.io/isithas-wiki/computer_science/programming_language_theory/types.md).

# types

## Basic idea

Static disciplines that classify program values and rule out classes of errors before execution. Type systems range from simple (Hindley-Milner) to dependent (Coq, Lean) — more expressive types catch more errors but cost more to check.

## Key formulas

* Typing judgement: $\Gamma \vdash e : \tau$
* Function type: $\tau\_1 \to \tau\_2$
* Universal type: $\forall \alpha.\ \tau$
* Curry-Howard: types ≅ propositions; programs ≅ proofs.