2018 | OriginalPaper | Chapter
A Primer on Type Systems
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.