Anti-symmetry of higher-order subtyping

Abstract

This paper shows that the subtyping relation of a higher- order lambda calculus, Fω≤, is anti-symmetric. It exhibits the first such proof, establishing in the process that the subtyping relation is a partial order—reflexive, transitive, and anti-symmetric up to β-equality. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. The result, which may seem obvious to the non- expert, is technically challenging, and had been an open problem for almost a decade. In this context, typed operational semantics for subty- ping offers a powerful new technology to solve the problem: of particular importance is our extended rule for the well-formedness of types with head variables. The paper also gives a presentation of Fω≤ without a re- lation for β-equality, apparently the first such, and shows its equivalence with the traditional presentation.