Search

This paper reports preliminary work on a novel approach to Coercive Subtyping that is based on relationships between reduction behaviour of source and target types in coerced terms. Coercive Subtyping is a superset of record-based subtyping, allowing so-called coercion functions to carry the subtyping. This allows many novel and powerful forms of subtyping and abbreviation, with applications including interfaces to theorem provers and programming with dependent type systems. However, the use of coercion functions introduces non-trivial overheads, and requires difficult proof of properties such as coherence in order to guarantee sensible results. These points restrict the practicality of coercive subtyping.We begin from the idea that coercing a value v from type U to a type T intuitively means that we wish to compute with v as if it was a value in T, not that v must be converted into a value in T. Instead, we explore how to compute on U in terms of computation on T, and develop a framework for mapping computations on some T to computations on some U via a simple extension of the elimination rule of T. By exposing how computations on different types are related, we gain insight on and make progress with several aspects of coercive subtyping, including (a) distinguishing classes of coercion and finding reasons to deprecate use of some classes; (b) alternative techniques for proving key properties of coercions; (c) greater efficiency from implementations of coercions.

The semantic structure of a polymorphic calculus λm is studied. λm is defined over a hierarchical type structure, and a function in this calculus, called a generic function, can be composed from more than one lambda expression and the ways it behaves on each type are weakly related in that it lax commutes with the coercion functions defined from the subtypes to the supertypes.Since laxness is intermediate between ad hocness (behaviors on each type are not related) and coherency (commuting with the coercion functions), λm has syntactic properties lying between those of calculi with ad hoc generic functions and coherent generic functions studied in Tsuiki (Math. Struct. Comput. Sci. 8 (1998) 321). That is, although λm allows self application and thus is not normalizing, it does not have any unsolvable terms. For this reason, all the semantic domains are connected by mutually recursive equations and, at the same time, they do not have the least elements.We solve them by considering fibrations and expressing the equations as a recursive equation about fibrations. We also show the adequacy theorem for λm following the construction of Pitts and use it to derive some syntactic properties.

We consider the problem of integrating XDuce into ML. This is difficult because of incompatible type and value representations. Our solution is a type-driven translation scheme from XDuce to ML based on a structured representation of XDuce values. XDuce type inference guides the insertion of appropriate coercion functions to translate regular expression pattern matching and uses of semantic subtyping. We can extend our translation scheme to include ML function calls and patterns into XDuce. Thus, we can embed XDuce into ML. Our results allow to enrich the ML language with support for dealing with semi-structured data.