Type Systems
Foundation: type systems for functional languages
Canonical functional language: the ?-calculus
M ::= c | x | (M M) | (?x M)
c ? C (a set of constants)
x ? V (a set of variables)
So the ?-calculus is really a family of languages that differ only in the constants and variables.
A simple type system for the ?-calculus.
- A type has the form
? ::= b | ? ? ?
b ? B (a set of base types)
- Augmented language syntax:
M ::= c | x | (M M) | (?x:? M)