Subtyping à la Church

Adriana Compagnoni
Stevens Institute of Technology

Healfdene Goguen
Google

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

PDF