Subtyping à la Church
Abstract
Type theories with higher-order subtyping or singleton types
are examples of systems where the computational behavior of variables is determined
by type information in the context. A complication for these systems is that
bounds declared in the context do not interact well with the logical relation
proof of completeness or termination. This paper proposes a simple modification
to the type syntax for F-omega-≤, adding a variable’s bound to the
variable type constructor, thereby separating the computational behavior of
the variable from the context. The algorithm for subtyping in F-omega-≤can
then be given on
types without context or kind information. As a consequence, the metatheory
follows the general approach for type systems without computational information
in the context, including a simple logical relation definition without Kripke-style
indexing by context. Completeness and correctness, anti-symmetry, transitivity
elimination and termination of the algorithm are all proved.
Full text