Types are semantic properties of program phrases. For instance, the type of an expression may model what type of value the expression would be evaluated to eventually, for example, the type of natural numbers or of Boolean values in an expression language. Types may be assigned to program phrases statically by means of a type system – this is a formal system consisting of inference rules, very much like a semantics definition. Assigned types (“properties”) must predict runtime behavior in a sound manner, i.e., the properties should never be violated by the actual runtime behavior. This is also referred to as type safety (or soundness). The rules making up a type system are easily implemented as type checkers, for example, in Haskell, as we will demonstrate. In this chapter, we provide a (very) basic introduction to type systems.
Unable to display preview. Download preview PDF.