= Type system
{wiki}
A <type system> assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching <programming language>, `int` admits <integer> addition, `bool` supplies `true` and `false` for conditions, and a <function type> specifies an argument type and a result type. Storage as <bits> alone does not explain these distinctions; the <type system> determines whether an expression can serve as an argument, a condition or an operand.
A <typing judgment> $\Gamma\vdash e:\tau$ says that expression $e$ has type $\tau$ under the assumptions in the <typing context> $\Gamma$. For example,
$$
\Gamma=\{x:\mathrm{int},y:\mathrm{int}\},\qquad \Gamma\vdash x+y:\mathrm{int}.
$$
The assumptions give each operand type `int`; the addition rule then gives the sum type `int`. Changing $y$ to type `bool` prevents this derivation. Our teaching <programming language> has distinct `int` and `bool` types and no implicit conversions between them.
The conditional rule requires a Boolean condition and the same type for both branches:
$$
\frac{\Gamma\vdash c:\mathrm{bool}\qquad\Gamma\vdash e_1:\tau\qquad\Gamma\vdash e_2:\tau}{\Gamma\vdash\mathrm{if}\ c\ \mathrm{then}\ e_1\ \mathrm{else}\ e_2:\tau}.
$$
Thus `if true then 1 else 2` has type `int`, while `if true then 1 else false` is rejected: its branches would require $\tau=\mathrm{int}$ and $\tau=\mathrm{bool}$ simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular <type system>; a different <programming language> can choose different rules. https://softwarefoundations.cis.upenn.edu/plf-current/Types.html[Software Foundations, Programming Language Foundations, Type Systems: typing relation]{ref}
The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The <function type> diagram shows this for a call. <Type inference> can discover the required types automatically, and <type variables> let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.
The guarantee depends on the rules and execution model. <Type safety> can exclude specified failures such as adding a Boolean or calling an <integer> as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A <type system> that permits unrestricted recursion can accept a computation that runs forever; <exception handling> also needs its own account of permitted outcomes.
Back to article page
