A record calculus based on symmetric concatenation

Abstract: "A number of different formulations of record calculi have been proposed. These may be broadly classified according to whether or not they are based on subsumption and whether they admit the specification of positive or negative information about record type variables. The systems considered by Wand (and their derivatives) may be classified as subsumption-free, negative information calculi. Early systems of bounded quantification are subsumption-based, and admit specification only of positive information. More recently, Cardelli and Mitchell have proposed a subsumption-based system featuring both positive and negative constraints, and, in earlier work, the authors have considered a subsumption-free variant. None of these systems copes well with the "symmetric merge" operation in which two records are considered mergeable only if they have no overlapping fields.To address this question, Cardelli and Mitchell suggest an extension to their subsumption-based calculus to admit mergeability constrains [sic]. In this paper we show that a subsumption-free calculus based only on mergeability constraints suffices not only for symmetric merge, but also for a wide class of other record operations. Moreover, the proposed calculus avoids some known difficulties with recursive types associated with positive-information calculi; in particular, the motivating examples for F-bounded quantification may be readily expressed without extending the language. A number of object oriented features, such as those considered by Wand and Buneman and Ohori, may also be represented naturally in this calculus."