Volume 6: January - December 1996

Issue 4: August 1996

Abstract


Inclusions and subtypes II: higher-order case

  • Inclusions and subtypes II: higher-order case
  • N. Marti-Oliet and J. Meseguer SRI International, Menlo Park, CA 94025, USA and Center for the Study of Language and Information, Stanford University, Stanford, CA 94305, USA. Email: {narciso, meseguer}@csl.sri.com

    ABSTRACT

    The first-order theory of subtypes as inclusions developed in Part I is extended to a higher-order context. This involves providing a higher-order equational logic for (inclusive) subtypes, a categorical semantics for such a logic that is complete and has initial models, and a proof that this higher-order logic is a conservative extension of its first-order counterpart. This higher-order categorical semantics includes a new notion of homomorphism between models that is both very natural in terms of its preservation properties and substantially more general than other notions of higher-order homomorphism proposed previously. The categorical semantics of higher-order inclusive subtypes is then generalized to a notion of model with two subtype relations [tau] <= [tau]' (inclusion) and [tau] <= : [tau]' (implicit conversion) thus reconciling and relating the two different intuitions that have so far prevailed in the first-order and higher-order cases. Axioms are then given that integrate the <= and <= : relations in the unified categorical semantics. Besides enjoying the benefits provided by each of the notions without their respective limitations, this framework supports rules for structural subtyping that are more informative and can discriminate between inclusions and implicit conversions.

    Keywords: Subtype, inclusion, coercion, overloading, typed [lambda]-calculus, Cartesian closed categories.

    Pages: 541 - 572

    Part of the OUP Journal of Logic and Computation WWW service


    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 09 Sep 96

    Part of the OUP Journals World Wide Web service.


    Copyright Oxford University Press, 1996