Coherence and transitivity in coercive subtyping

Abstract

The aim of this thesis is to study coherence and transitivity in coercive subtyping. Among other things, coherence and transitivity are key aspects for a coercive subtyping system to be consistent and for it to be implemented in a correct way. The thesis consists of three major parts. First, I prove that, for the subtyping rules of some parameterised inductive data types, coherence holds and the normal transitivity rule is admissible. Second, the notion of weak transitivity is introduced. The subtyping rules of a large class of parameterised inductive data types are suitable for weak transitivity, but not compatible with the normal transitivity rule. Third, I present a new formulation of coercive subtyping in order to combine incoherent coercions for the type of dependent pairs. There are two subtyping relations in the system and hence a further understanding of coherence and transitivity is needed. This thesis has the first case study of combining incoherent coercions in a single system. The thesis provides a clearer understanding of the subtyping rules for parameterised inductive data types and explains why the normal transitivity rule is not admissible for some natural subtyping rules. It also demonstrates that coherence and transitivity at type level can sometimes be very difficult issues in coercive subtyping. Besides providing theoretical understanding, the thesis also gives algorithms for implementing the subtyping rules for parameterised inductive data types.