Technical report version.
Type dispatch constructs are an important feature of many programming languages. Scheme
has predicates for testing the runtime type of a value. Java has a class cast
expression and a try statement for switching on an exception's class. Crucial to these
mechanisms, in typed languages, is type refinement: The static type system will use type
dispatch to refine types in successful dispatch branches. Existing work in functional
languages has addressed certain kinds of type dispatch, namely, intensional type analysis.
However, this work does not extend to languages with subtyping nor to named types.
This paper describes a number of type dispatch constructs that share a common theme: class
cast and class case constructs in object oriented languages, ML style exceptions,
hierarchical extensible sums, and multimethods. I describe a unifying mechanism, tagging,
that abstracts the operation of these constructs, and formalise a small tagging language.
After discussing how to implement the tagging language, I present a more primitive
language and give a formal translation from the tagging language.