A reduction is a syntactic mapping of a higher-level definition to a series of lower-level definitions. The lower-level definitions can be taken as the detailed, concrete meaning of the higher-level one. Further, the typing of the lower-level definitions implies a sound typing of the higher-level one.
This reduction includes a first-class class object, a runtime representation of a class that can be passed to functions and stored in data structures; the reduction also yields a class object type whose instances are the class objects of this class and its subclasses.
We take the approach that complex virtual fields have exact and general aspects. The exact aspect of a field describes its implementation, while its general aspect constrains the ways in which the field can be overridden. We describe how a class body maps to these aspects and how these aspects relate to typing. In particular, the reduction yields two types per class C: the exact type, C@, provides type-safe access to all fields, while the general type, C#, supports subclass polymorphism.
Presented at FOOL 2011; Sunday, 23 October 2011; Portland, Oregon, USA