Type Systems
Typing rules for the (simply) typed ?-calculus
Each constant c ? C has a given type ?(c)
Since an expression M inside a ?-calculus program may contain free variables, type rules keep track of the types of these variables using a type environment ? ? V ? T where T denotes the set of types ?. This type environment is simply a symbol table that records a symbol’s type!
Assume M:? ? ? and N: ? . Then (M N): ?.
Assume x: ? implies that M: ?. Then (?x: ? M): ? ? ?.
The process of assigning types to ?-calculus programs can be rigorously formalized as a
natural deduction system where the formal sentences are typing judgements of the form
? |- M: ? and the mechanisms for generating true sentences are
- axioms of the form ? |- M: ? and
- inference rules of the form
?1 |- M1: ?1, …, ?N |- MN: ?N ? ? |- M: ?