[1]: 94 These rules may be applied by the type system to determine if a program is well-typed and what type expressions have.
A prototypical example of the use of typing rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.
[1]: 92 Syntactically, the typing relation is usually denoted by a colon, so for example
The rules themselves are usually specified using the notation of natural deduction.
[1]: 26 For example, the following typing rules specify the typing relation for a simple language of booleans:[1]: 93 Each rule states that the conclusion below the line may be derived from the premises above the line.
The first two rules have no premises above the line, so they are axioms.
In programming languages, the type of a variable depends on where it is bound, which necessitates context-sensitive typing rules.
These rules are given by a typing judgment, usually written
This notation can be used to give typing rules for variable references and lambda abstraction in the simply typed lambda calculus:[1]: 101–102 Similarly, the following typing rule describes the
construct of Standard ML: Not all systems of typing rules directly specify a type checking algorithm.
For example, the typing rule for applying a parametrically polymorphic function in the Hindley–Milner type system requires "guessing" the appropriate type at which the function should be instantiated.
[3] Adapting a declarative rule system to a decidable algorithm requires the production of a separate, algorithmic system that can be proven to specify the same typing relation.
[4] This programming language theory or type theory-related article is a stub.