Structural Semantics for Polymorphic Data Types

Abstract

The semantic modeling of data types has been the subject ofincreased interest over the last few years, enhanced by thedevelopment of applicative languages such as Edinburgh's ML andHOPE, by the need for flexible highly structured languages thatwould nonetheless be amenable to verification, and by ongoinginquiries on polymorphism in programming languages. In particular,there has been a growing interest in generic type structures suchas the Reynolds-Girard discipline of full polymorphism, furtherextended by McCracken [McC] and MacQueen and Sethi [MS], and inuser-defined and recursively-defined types.Our aim here is to model semantically the notion of type so asto encompass full polymorphism, but in a very controlled way whichon the one hand allows the modeling to remain simple, and on theother hand conveys as much of the notion of type as seems feasiblyrelevant to programming languages.Our leading idea is that a type is a structural condition ondata objects rather than a collection of objects which satisfiescertain closure properties. Roughly, we argue that such structuralconditions are fully conveyed by syntactic expressions, not inisolation of course, but within a syntax-oriented typediscipline. In other words, we treat types as discrete objects,which merely code the ways data objects are allowed to interact (asin applying functional object a to object b). Once atype discipline is set to delineate a set of type expressions, andonce the meaning of the type-constructs is imposed on the ways thedata objects relate, the meaning of each type expression isconveyed by the expression itself (reduced to a canonical form ifnecessary). This conception of types permits a strikingly simplemodeling of the use of types as arguments of data objects, a usecentral to Reynolds' polymorphic type system [Rey].The use of types as genuine arguments of procedures is notdevoid of practical interest. E.g., one may wish to treat objectsof type o generically, except for an initial choice dependingon the principal type-constructor of o, that is, according towhether o is an atomic type, a functional type, a cartesianproduct, etc.A particular situation where such choices may be useful is wherea procedure has a formal parameter intended to range over some datastructure (trees of sequences of objects of type t, say), adata structure that has a number of accepted representations byformal data types. It seems desirable to permit the definition of apolymorphic procedure that would accept as valid a number of suchformal representations, branching on them internally. This kind offacility would elevate the polymorphism of a procedure from thelevel of uses with in a single program, to the level oftransportability from one set of data structure specifications toanother.This kind of use of types as arguments is compatible withReynold's discipline of type abstraction, but not with thequantificational discipline of [MS] (cf.[Lei83], §4.2). Whilethe two disciplines, as uninterpreted and unexpanded calculi, arecombinatorially isomorphic the difference between their intendedsemantics becomes apparent when primitive functions over types(such as discriminators over main type-constructor) areconsidered.The examples we have given of uses of types as arguments arefairly restricted in nature: all that is used of a type is itssyntactically representable structure. This is not merely anempirical observation on our limited perception at present time. Ina typed discipline of programming each object carries its type(explicitly or not), and all types of denotable objects arethemselves denotable. It follows that any question that one may askabout the type of a denotable object reduces to a question abouttype-expression(s) denoting that type. The issue of semanticallymodeling Reynold's rich discipline of type abstraction is thereforereduced, from a pragmatic point of view, to a modeling in whichquestions about types are all expressible as questions about typeexpressions.Existing approaches to the semantic modeling of data types are,in one form or another, conceptual continuations of thedenotational semantics approach to data objects. McCracken [McC],following [Sco], defines types as retracts of the universal domain.In Shamir and Wadge [SW], Milner [Mil] and MacQueen and Sethi [MS]types are modeled as some kind of ideal, where an ideal is asubset of the object-domain that satisfies certain closureconditions. In both approaches types are being defined via theproperties that they must satisfy, as sets of objects, so as tobecome compatible with their use. (This may be compared with thealgebraic approach to types, where each particular type isdefined via its algebraic properties rather than its intendedconception).Our modeling of types too is grafted on top of a denotationalsemantics for the object language, However,it has a life of itsown, and can be explained in isolation, or combined with forinstance, an operational semantics for the object language. Thepoint we are trying to make is that the semantics of types haslittle to do with the issues of self-application and continuitywhich motivate denotational semantics. Rather than amalgamateobjects and types, as in [SW] (where types as sets of objects aretreated on an equal footing with objects as sets ofapproximations), we separate the two radically.We make no claim, of course, that our approach should supplantthe modeling of types as retracts or as ideals. Rather, we believethat the semantics we propose is related to types-as-ideals in muchthe same way as operational semantics is related to denotationalsemantics: it is closer to programming practice, permits a smallerset of objects, and is sensitive to the choice of formal framework(which for us is the type discipline). We therefore feel that thetwo approaches should shed light on each other and, in combination,enhance our understanding of complex data-types and and theirproper use.In particular, we believe that even putting down the definitionsand proving basic existence theorems provides some insight aboutthe design and use of data types. For one, our modeling of typessuggests a feasible controlled use of types as arguments of dataobjects. For another, it points to directions in setting very richtype disciplines evolving naturally from a structural-computationalview of types. For instance, it may be useful and feasible toconsider types built as certain recursive sets of other types.Following preliminaries in sections 1 and 2 we define in section3 what is a model of the pure polymorphic lambda calculus.A termmodel is constructed in §4,in §5 we show how to constructa non-extensional model through the solution of a domain equation,and in §6 we construct an extensional model through such asolution. The latter construction involves breaking the circularityin the conditions underlying polymorphic typing, by a method akinto Girard's in the proof theory of higher order logic [Gir].We plan to extend this work in two directions. One is thetreatment of more general type disciplines, of the kinds defined byMcCracken [McC] and further studied by MacQueen and Sethi [MS]. Thecrucial issue here is that, in contrast to Reynold's discipline,distinct type expressions may denote the same type. However, eachtype expression has a normal form, which may be viewed as itsvalue (this view has been advocated in greater generality by PerMartin-Lof [Mar], on somewhat more philosophical grounds). A seconddirection, incorporating aspects of the first, is the treatment ofrecursively defined data types in a polymorphic context, andpossibly more general notions of types.