About the completeness of type systems

Kahrs, Stefan (1996) About the completeness of type systems. In: UNSPECIFIED.

PDF
 Preview
Postscript
The original purpose of type systems for programming languages was to prevent certain forms of run-time errors, like using a number as a function. Some type systems go as far as guaranteeing the absence of run-time errors, e.g. the type system of Standard ML. One can call such a type system sound''. This raises the question of the dual notion of completeness, i.e. is everything typable that does not have run-time errors? Or, to put it in another way: does the type system restrict the expressive power of the underlying implementation in an undesirable way? To make this rather vague idea precise we define an abstract notion of type system'', together with general notions of soundness and completeness. We examine several type systems for these properties, for instance ?<sup>?</sup> and PCF are both complete, but for very different reasons.