Inclusions and subtypes II: Higher-order case

Narciso Martí-Oliet, José Meseguer

Research output: Contribution to journalArticle

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 τ ≤ τ′ (inclusion) and τ ≤: τ′ (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.

Original languageEnglish (US)
Pages (from-to)541-572
Number of pages32
JournalJournal of Logic and Computation
Volume6
Issue number4
DOIs
StatePublished - Aug 1996
Externally publishedYes

Keywords

  • Cartesian closed categories
  • Coercion
  • Inclusion
  • Overloading
  • Subtype
  • Typed λ-calculus

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Fingerprint Dive into the research topics of 'Inclusions and subtypes II: Higher-order case'. Together they form a unique fingerprint.

  • Cite this