A Reflective Domain Construction for Type Inheritance and Higher-Order Generics

Summary A semantic domain that captures the notions of type inheritance and higher-order generic functions is constructed. Here, a type is defined to inherit another type if a coercion function exists between them. A function is defined as generic if it preserves types and coercions. It is constructed in the category of I-domains (domain with type inheritance), whose objects are mathematical models of domains with hierarchical type structure. Their morphisms are mathematical models of generic functions. This category is Cartesian closed, and domain equations such as M = M B + [ M ↕ M ] are solvable in this category. In the solution of this equation, the semantics of untyped lambda calculus with generic constants is defined.