¡£¢¥¤§¦©¨¤¤ "! #$¤§%&#(')¡0123¢546078¢9049@A% ¡£¢¥@B¢5¤ CEDGF8HICEPQDSR5T U F6VWVPXRYa`HcbXR3V d)e R3f Uhg eieWprq R3ViV sutwvyx€9vƒ‚ „ … g DS†AbBVWR eu‡‰ˆ3p R ˆ R d‘e g bX† ’ F ei“ F e T•”E p–“ R eWqip Vƒ— … F8D™˜ ep TXfR8d U F qiq F ˆ P‰b q RViV q A Step-Indexed Model of Substructural State Amal Ahmed Harvard University amal@eecs.harvard.edu Matthew Fluet ∗ Cornell University fluet@cs.cornell.edu Greg Morrisett ∗ Harvard University greg@eecs.harvard.edu Abstract The concept of a “unique” object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to ensure that some obligation will be met (e.g., an opened file will be closed). However, different languages provide different interpretations of “uniqueness” and have different rules regarding how unique objects interact with the rest of the language. Our goal is to establish a common model that supports each of these languages, by allowing us to encode and study the interactions of the different forms of uniqueness. The model we provide is based on a substructural variant of the polymorphic λ-calculus, augmented with four kinds of mutable references: unrestricted, relevant, affine, and linear. The language has a natural operational semantics that supports deallocation of references, strong (type-varying) updates, and storage of unique objects in shared references. We establish the strong soundness of the type system by constructing a novel, semantic interpretation of the types. This technical report is really two documents in one: The first part is a paper appearing in the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP’05). The second part is a formal development of the language, step-indexed model, and soundness proof referenced in the first part. If you have already read a version of “A Step-Indexed Model of Substructural State”, then you should proceed directly to the appendices. 1. Introduction Consider the following imperative code fragment, written with SML syntax: 1. fun f(r1:int ref, r2:int ref):int = 2. (r1 := true ; 3. !r2 + 42) At line 1, we assume ref cells r1 and r2 whose contents are integers. At line 2, we update the first cell with a boolean. Then, at line 3, we read the second cell, using the contents in a context expecting an integer. If the function is called with actual arguments that are different ref cells, then there is nothing in the function that will cause a run-time type error.1 Yet, if the same ref cell is passed for each formal argument, then the update on line 2 will change the contents of both r1 and r2, causing a run-time type error to occur at line 3. SML (and most imperative languages) reject the above program, because references are unrestricted, that is, they may be freely aliased. In general, reasoning about unrestricted references is hard because we need additional information to understand what other values are affected by an update. In the absence of this information, we must be conservative. For instance, in SML, we must assume that an update to an int ref could affect any other int ref. To ensure type soundness, we must therefore require the type of the ref’s contents be preserved by the update. In other words, most type systems can only track invariants on refs, instead of program-point-specific properties. As a result, we are forced to weaken the type of the ref to cover all possible program points. In the example above, we must weaken r1’s type to “(int + bool) ref” and pay the costs of tagging values, and checking those tags when the pointer is dereferenced. Unfortunately, in many settings, this weakened invariant is insufficient. Hence, researchers have turned to more powerful systems that do provide a means of ensuring exclusive access to state. In particular, many projects have introduced some form of linearity to “tame” state. Linear logic [15] and other substructural logics give rise to more expressive type systems, because they are designed to precisely account for resources. ∗ This material is based upon work supported by the Air Force Office of Scientific Research under Award No. F49620-03-1-0156 and Award No. F4962001-1-0298 and by the Office of Naval Research under Award No. N00014-01-1-0968. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not necessarily reflect the views of these organizations or the U.S. Government. 1 We assume that values are represented uniformly so that, for instance, unit, booleans, and integers all take up one word of storage. 1 2005/7/8 For instance, the Clean programming language [26] relies upon a form of uniqueness to ensure equational reasoning in the presence of mutable data structures. The Cyclone programming language [17] uses unique pointers to allow fine- grained memory management. For example, a unique pointer may be updated from uninitialized to initialized, and its contents may also be deallocated: 1. x = malloc(4); // x: --- *‘U 2. *x = 3; // x: int *‘U 3. free(x); // x: undefined In both of these languages, a unique object may be implicitly discarded, yielding a weak form of uniqueness called affinity. The Vault programming language [13] uses tracked keys to enforce resource management protocols. For example, the following interface specifies that opening a file returns a new tracked key, which must be present when reading the file, and which is consumed when closing the file: 1. interface IO { 2. type FILE; 3. tracked($F) FILE open(string) [ +$F ]; 4. char read (tracked($F) FILE) [ $F ]; 5. void close (tracked($F) FILE) [ -$F ]; } Because tracked keys may be neither duplicated nor discarded, Vault supports a strong form of uniqueness technically termed linearity, which ensures that an opened file must be closed exactly once. Other projects [32, 12] have also incorporated linearity to ensure that memory is reclaimed. Both forms of uniqueness (linearity and affinity) support strong updates, whereby the type of a stateful object is changed in response to stateful operations. For example, the Cyclone code fragment above demonstrates the type of the unique pointer changing from uninitialized to initialized (with an integer) in response to the assignment. The intuitive understanding is that a unique object cannot be duplicated, and thus there are no aliases to the object; hence, no other portion of the program may observe the change in the object’s type, so it is safe to perform a strong update. Yet, programming in a language with only unique (i.e., linear or affine) objects is much too painful. In such a setting, one can only construct tree-like data structures. Hence, it is not surprising that both Cyclone and Vault allow a programmer to put unique objects in shared objects, with a variety of restrictions to ensure that these mixed objects behave in a safe manner. In fact, understanding the various mechanisms by which unique objects (with strong updates) may safely coexist and mix with shared objects is currently an active area of research [5], though much of it has focused on high-level programming features, often without a complete formal account. Therefore, it is natural to study a core language with mutable references of all sorts mentioned above: linear, affine, and unrestricted. The study of substructural logics immediately suggests one more sort — relevant, which describes data that may be duplicated but not implicitly discarded. Having made these distinctions, a number of design questions arise: What does it mean to duplicate or to discard a reference? What operations may be safely performed with the different sorts of references? What combinations of sorts for a reference and its contents are safe? A major contribution of this paper is to answer these questions, giving an integrated design of references for all of these substructural sorts (Section 3). Our design allows unique (linear and affine) values to be stored in shared (unrestricted and relevant) references, while preserving the desirable feature that resources are tracked accurately. Our language extends a core λ-calculus with a straightforward type system that provides data of each of the substructural sorts mentioned above (Section 2). The key idea, present in other substructural type systems, is to break out the substructural sorts as type “qualifiers.” Rather than prove soundness via a syntactic subject-reduction proof, we adopt an approach compatible with that used in Foundational Proof Carrying Code [6, 7]. We construct a step-indexed model (Section 4) where types are interpreted as sets of store description / value pairs, which are further refined using an index representing the number of steps available for future evaluation. We believe this model improves on previous models of mutable state, contributing a compositional notion of aliasing and ownership that directly addresses the subtleties of allowing unique values to be stored in shared references. Furthermore, we achieve a simple model, in comparison to denotational and domain-theoretic approaches, that easily extends to impredicative polymorphism and first-class references. Constructing a (well-founded) set-theoretic model means that our soundness and safety proofs are amenable to formalization in the higher-order logic of Foundational PCC. Hence, our work provides a useful foundation for future extensions of Foundational PCC, which currently only supports unrestricted references, but is an attractive target for source languages wishing to carry high-level security guarantees, enforced by type states and linear resources, through to machine code. 2. λURAL: A Substructural λ-Calculus Advanced type systems for state rely upon limiting the ordering and number of uses of data and operations to ensure that state is handled in a safe manner. For example, (safely) deallocating a data structure requires that the data structure is never 2 2005/7/8 Kind Level: Kinds κ ::= QUAL | | Type Level: Constant Qualifiers q ∈ Quals = {U, R, A, L} Qualifiers ξ ::= α | q PreTypes Types τ ::= α | 1 | τ1 τ2 | τ1 τ2 | ∀α:κ. τ τ ::= α | ξτ Type-level Terms ι ::= ξ | τ | τ Expression Level: Values Expressions v ::= x | | v1, v2 | λx. e | Λ. e e ::= v | let = e1 in e2 | let x1, x2 = e1 in e2 | e1 e2 | e [] Figure 1. λURAL Syntax used in the future. In order to establish this property, a type system may ensure that the data structure is used at most once; after one use, the data structure may be safely deallocated, since there can be no further uses. A substructural type system provides the core mechanisms necessary to restrict the number and order of uses of data and operations. A conventional type system, such as that employed by the simply-typed λ-calculus, with a typing judgement like Γ e : τ , satisfies three structural properties: Exchange If Γ1, x:τx, y:τy, Γ2 e : τ , then Γ1, y:τy, x:τx, Γ2 e : τ . Contraction If Γ1, x:τz, y:τz, Γ2 e : τ , then Γ1, z:τz, Γ2 e[z/x][z/y] : τ . Weakening If Γ e : τ , then Γ, x:τx e : τ . In contrast, a substructural type system is designed so that one or more of these structural properties do not hold in general. Among the most widely studied substructural type systems are the linear type systems [29, 24], derived from Girard’s linear logic [15], in which all variables satisfy Exchange, but linearly typed variables satisfy neither Contraction nor Weakening. In this section, we present a substructural polymorphic λ-calculus, similar in spirit to Walker’s linear lambda calculus [30]. In our calculus, types and variables are qualified as unrestricted (U), relevant (R), affine (A), or linear (L). All variables will satisfy Exchange, while only unrestricted variables will satisfy both Contraction and Weakening, allowing such variables to be used an arbitrary number of times. We will require • linear variables to satisfy neither Contraction nor Weakening, ensuring that such variables are used exactly once, • affine variables to satisfy Weakening (but not Contraction), ensuring that such variables are used at most once, and • relevant variables to satisfy Contraction (but not Weakening), ensuring that such variables are used at least once.2 The diagram below demonstrates the relationship between these qualifiers, inducing a lattice ordering . linear  (?L??)?1 affine (?A??)?1 relevant (R)  unrestricted (U) 2.1 Syntax Figure 1 presents the syntax for our core calculus, dubbed the λURAL-calculus. Most of the types, expressions, and values are based on a traditional polymorphic λ-calculus. Kind and Type Levels We structure our types τ as a qualifier ξ applied to a pre-type τ , yielding the four sorts of types noted above. The qualifier of a type dictates the structural operations that may be applied to values of the type, while the pre-type dictates the introduction and elimination forms. The pre-types 1 , τ1 τ2, and τ1 τ2 correspond to the unit, pair, and function types of the polymorphic λ-calculus. Polymorphism over qualifiers, pre-types, and types is provided by a single pre-type ∀α:κ. τ ; we introduce a kind level to distinguish among the type-level terms that may be used to instantiate a polymorphic pre-type (with kinds QUAL, , and for qualifiers, pre-types, and types, respectively). 2 In the logic community, it is perhaps more accurate to use the qualifier “strict” for such variables. However, “strict” is already an overloaded term in the functional programming community; so, like Walker [30], we use “relevant.” 3 2005/7/8 In the appendicies, we also include additive unit (1 ), additive pair (τ1 τ2), void (0), sum (τ1 τ2), existential (∃α:κ. τ ), and recursive (µα: . τ ) pre-types and recursive functions in the calculus, though we elide such constructs in this expository development. This structuring of types as a qualifier applied to a pre-type follows that of Walker [30], but differs from other presentations of linear lambda calculi that use exactly one modality (!τ ) to distinguish unrestricted from linear types. It seems possible to introduce alternative modalities (e.g, −τ for affine and +τ for relevant), but then we would have to consider their interaction (e.g., what does −!+τ denote?). Also, with four distinct qualifiers, it is natural to introduce qualfier polymorphism, which is best formulated by separating qualifiers from pre-types. Expression Level Each pre-type has an associated value introduction form. The pattern matching expression forms let = e1 in e2 and let x1, x2 = e1 in e2 are used to eliminate units (1 ) and pairs ( ), respectively. As usual, a function with pre-type τ1 τ2 is eliminated via application e1 e2, while a type-level abstraction ∀α:κ. τ is eliminated via instantiation e []. Note that expressions are not decorated with type-level terms. This simplifies the semantic model presented in Section 4, where soundness is with respect to typing derivations, and is appropriate for an expressive “internal” language. We leave as an open problem the formulation of appropriate inference and elaboration algorithms yielding derivations in the type system of the next section, which would likely require some type-level annotations on expressions in a “surface” language. 2.2 Static Semantics The goal of the type system for λURAL is to approximate the requirements of languages like Vault and Cyclone, which ensure that linear values are used exactly once, affine values are used at most once, and relevant values are used at least once. Dually, the type system should ensure that only unrestricted and relevant values are duplicated and only unrestricted and affine values are discarded. To prevent values from being implicitly copied or dropped when their containing value is duplicated or discarded, the type system must also ensure that a (functional) value with a qualifier lower in the lattice may not contain values with qualifiers higher in the lattice. For example, an affine (A) pair may not contain linear (L) components, since we could end up dropping the linear components by dropping the pair, so the type sytem must rule out expressions of type A(Lτ 1 Lτ 2). Despite these requirements, the type system is relatively simple. λURAL typing judgements have the form ∆; Γ e : τ where the contexts ∆ and Γ are defined as follows: Type-level Term Context ∆ ::= • | ∆, α:κ Value Context Γ ::= • | Γ, x:τ Thus, ∆ is used to track the set of type-level variables in scope (along with their kinds), whereas Γ, as usual, is used to track the set of (expression-level) variables in scope (along with their types). There may be at most one occurrence of a type-level variable α in ∆ and, similarly, at most one occurrence of a variable x in Γ. Figure 2 presents the λURAL kinding rules and Figure 3 presents the λURAL typing rules. In order to ensure the correct relationship between a data structure and its components, we extend the lattice ordering on constant qualifiers to types and contexts (see Figure 4). In the presence of qualifier and type polymorphism, we include the rules ∆ U α and ∆ α L, a conservative extension, since U and L are the bottom and top of the lattice. A more general approach would incorporate bounded qualifier constraints, which we believe is straightforward, but doing so does not add to the discussion at hand. As is usual in a substructural setting, our type system relies upon a judgement ∆ Γ ; Γ1 Γ2 that splits the assumptions in Γ between the contexts Γ1 and Γ2 (see Figure 5). Splitting the context is necessary to ensure that variables are used appropriately by sub-expressions. Note that ensures that an A or L assumption appears in exactly one subcontext. On the other hand, U and R assumptions may appear in both sub-contexts, corresponding to implicit duplication of the variables. The rule (MPair) is representative: the context is split by to type each of the pair components, and the types of each component are bounded by the qualifier assigned to the pair. Intuitively, the L and A assumptions in the context are exclusively “owned” by exactly one of the two components. Likewise, in the rule (Fn), the free variables of Γ, which constitute the closure of the function, must be bounded by the qualifier assigned to the function. Note that the qualifier assigned to a function type is unrelated to the types of the argument and result; rather, it is related to the abstracted components that are used when the function is executed. The rule (Weak) splits the context into a sub-context used to type the expression e and a discardable sub-context, consisting of U and A variables, that are not required to type the expression. Note that the rule (Weak) acts as a strengthened Weakening property, allowing an arbitrary number of U and A variables to be dropped at once. The corresponding strengthened Contraction property is incorporated into the judgement ∆ Γ ; Γ1 Γ2, which allows an arbitrary number of U and R variables to be copied at once. 4 2005/7/8 ∆ ι:κ α:κ ∈ ∆ (VarKn) ∆ α:κ (Qual) ∆ q : QUAL ∆ ξ : QUAL ∆ τ : (Type) ∆ ξτ : (MUnitPTy) ∆ 1: ∆ (MPairPTy) τ1 : ∆ τ2 : ∆ τ1 τ2 : ∆ (FnPTy) τ1 : ∆ τ2 : ∆ τ1 τ2 : ∆, α:κ τ : (AllPTy) ∆ ∀α:κ. τ : Figure 2. λURAL Statics (Kinding Rules) ∆; Γ e : τ ∆ τ: (Var) ∆; •, x:τ x : τ ∆ ξ : QUAL (MUnit) ∆; • : ξ1 ∆ Γ ; Γ1 Γ2 ∆ ξ : QUAL ∆; Γ1 v1 : τ1 ∆ τ1 ξ (MPair) ∆; Γ2 v2 : τ2 ∆ τ2 ξ ∆; Γ v1, v2 : ξ(τ1 τ2) ∆ (Fn) ξ : QUAL ∆ Γ ξ ∆; Γ, x:τ1 ∆; Γ λx. e : ξ(τ1 τ2) e : τ2 ∆ ξ : QUAL ∆ Γ ξ ∆, α:κ; Γ e : τ (All) ∆; Γ Λ. e : ξ∀α:κ. τ ∆ Γ ; Γ1 Γ2 (Let-MUnit) ∆; Γ1 e1 : ξ1 ∆; Γ2 e2 : τ ∆; Γ let = e1 in e2 : τ (Let-MPair) ∆; Γ1 ∆ Γ ; Γ1 Γ2 e1 : ξ(τ1 τ2) ∆; Γ2, x1:τ1, x2:τ2 ∆; Γ let x1, x2 = e1 in e2 : τ e2 : τ ∆ (App) Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξ(τ1 τ2) ∆; Γ e1 e2 : τ2 ∆; Γ2 e2 : τ1 ∆; Γ e : ξ∀α:κ. τ ∆ ι : κ (Inst) ∆; Γ e [] : τ [ι/α] ∆ (Weak) Γ ; Γ1 Γ2 ∆; Γ1 e : τ ∆; Γ e : τ ∆ Γ2 A Figure 3. λURAL Static Semantics (Typing Rules) ∆ ξ1 ξ2 ∆ α : QUAL ∆U α ∆τ ξ ∆ α: ∆α L q1 q2 ∆ q1 q2 ∆ α : QUAL ∆α L ∆ ξ : QUAL ∆ξ ξ ∆Γ ξ ∆ τ: ∆ξ ∆ ξτ ξ ξ ∆ ξ : QUAL ∆• ξ Figure 4. λURAL Statics (Sub-Qual Rules) ∆ ξ1 ξ ∆ ξ ∆ ξ1 ξ2 ξ2 ∆Γ ξ ∆τ ξ ∆ Γ, x:τ ∆ Γ ; Γ1 Γ2 ∆ •;• • ∆ Γ ; Γ1 Γ2 ∆ τ : ∆ Γ, x:τ ; Γ1, x:τ Γ2 ∆ Γ ; Γ1 Γ2 ∆ τ : ∆ Γ, x:τ ; Γ1 Γ2, x:τ Figure 5. λURAL Statics (Context Split Rules) ∆ Γ ; Γ1 Γ2 ∆ τ R ∆ Γ, x:τ ; Γ1, x:τ Γ2, x:τ 5 2005/7/8 Store s ::= {l1 → v1, . . . , ln → vn} (let-munit) (let-mpair) (app) (inst) (new) (free) (read) (write) (swap) (ctxt) (s, let = in e) −→ (s, e) (s, let x1, x2 = v1, v2 in e) −→ (s, e[v1/x1][v2/x2]) (s, (λx. e) v) −→ (s, e[v/x]) (s, (Λ. e) []) −→ (s, e) (s, new v) −→ (s {l → v}, l) (s {l → v}, free l) −→ (s, v) (s {l → v}, rd l) −→ (s {l → v}, l, v ) (s {l → v1}, wr l v2) −→ (s {l → v2}, l) (s {l → v1}, sw l v2) −→ (s {l → v2}, l, v1 ) (s, e) −→ (s , e ) (s, E[e]) −→ (s , E[e ]) Figure 6. λrefURAL Operational Semantics 3. λrefURAL: A Substructural λ-Calculus with References Languages like Vault and Cyclone include objects that change state (e.g., file descriptors), so it is natural to include some stateful values. We consider the difficult case of references, which can serve as mutable containers for both functional values and stateful values. Hence, we extend the λURAL-calculus with mutable references, to yield the λrefURAL-calculus. The reference pre-type ref τ may be combined with a qualifier ξ to yield the four sorts (U, R, A, L) of references discussed earlier. We also introduce operations to allocate (newq) and deallocate (free) references, as well as to read (rd), write (wr), and swap (sw) their contents. Not all of these operations can be safely performed with all sorts of references, as we discuss in Section 3.2. The syntactic extensions to support references are as follows: Type Level: PreTypes τ ::= . . . | ref τ Expression Level: Locations l ∈ Values v ::= Expressions e ::= Locs ... | l . . . | newq e | free e | rd e | wr e1 e2 | sw e1 e2 3.1 Operational Semantics Figure 6 gives the small-step operational semantics for λrefURAL as a relation between configurations of the form (s, e), where s is a global store mapping locations to qualifiers and values.3 The notation s1 s2 denotes the disjoint union of the stores s1 and s2; the operation is undefined if the domains of s1 and s2 are not disjoint. We use evaluation contexts E (omitted in this presentation) to lift the primitive rewriting rules to a standard, left-to-right, innermost-to-outermost, call-by-value interpretation of the language. Most of the rules are standard, so we highlight only those involving references. The expressions newq e and free e perform the complementary actions of allocating and deallocating mutable references in the global store. Specifically, the expression newq e evaluates e to a value v, allocates a fresh (unallocated) location l to store the qualifier q and value v, and returns l. The expression free e performs the reverse: it evaluates e to a location l, deallocates l, and returns the value previously stored at l. The expressions for reading and writing a mutable reference implicitly duplicate and discard (respectively) the contents of the reference. The expression rd e evaluates e to a location l, duplicates the value v stored at l, and returns l, v , leaving the value stored at l unchanged. Meanwhile, wr e1 e2 evaluates e1 to a location l and e2 to value v2, stores v2 at location l, discards the value previously stored at l, and returns l. In languages with only unrestricted (ML-style) references, it is customary for rd to return only the contents of l and for wr to return . However, we do not wish to consider reading or writing a linear (resp. affine) reference as the exactly-oneuse (resp. at-least-one-use) of the value. Therefore, the rd and wr (and sw) operations return the location l that was read or written, which remains available for future use. The behavior of ML-style references may be recovered by implicitly discarding the returned location. 3 We write squal(l) and sval(l) for the respective projections of s(l). 6 2005/7/8 Ref Ops Contents and Ops 8>>>< U URAL newU (weak updates) rd wr wr sw shared >>>: 8>>>< R A sw rd newR wr rd wr sw (weak updates) sw sw sw newA rd free wr wr sw >>>:unique sw(strong updates) L newL rd rd wr free wr sw sw sw sw(strong updates) Figure 7. Operations for Substructural State The expression sw e1 e2 combines the operations of dereferencing and updating a mutable reference, but has the attractive property that it neither duplicates nor discards a value. Notice that performing a write or swap operation on a location may change the type of the location’s contents. The static semantics will permit weak (type-invariant) updates on all references (with some additional caveats), but will restrict strong (type-varying) updates to unique references. The reader may well wonder why each reference is “stamped” with a qualifier at its allocation when the remainder of the operational rules are entirely agnostic with respect to a reference’s qualifier. Essentially, the qualifier is a form of instrumentation, which, when combined with the semantic model presented in Section 4, allows us to guarantee that linear and relevant references cannot be implicitly discarded. Such a property is difficult to capture exclusively in the operational semantics (i.e., by ensuring that the abstract machine “gets stuck” when a linear or relevant reference is implicitly dropped). On the other hand, the abstract machine does “get stuck” when attempting to access a reference after it has been deallocated. 3.2 Static Semantics As with the type system for λURAL, we would like the type system for λrefURAL to ensure the property that no linear or affine value is implicitly duplicated and no linear or relevant value is implicitly discarded. With that in mind — and noting that only unrestricted and relevant references may be implicitly copied (by the ∆ Γ ; Γ1 Γ2 judgement), while only unrestricted and affine references may be implicitly dropped (by the (Weak) rule) — we now answer the questions we laid out in Section 1: What operations may be safely performed with the different sorts of references? What combinations of sorts for a reference and its contents are safe? These answers are summarized in Figure 7. First, consider what it means to duplicate a reference. Operationally, a reference is a location in the global store. Therefore, duplicating an unrestricted or relevant reference l, simply yields two copies of l — while the value stored at l is not duplicated. Since duplicating a shared reference does not alter the uniqueness of its contents, it is not only reasonable but also extremely useful to allow shared references to store unique values. In particular, it permits the sharing of (large) unique data structures without expensive copying. On the other hand, dropping an unrestricted or affine reference l effectively drops its contents, since this reference may (must, in the case of affine) have been the only copy of l. If the contents were a linear or relevant value, then the exactlyone-use and at-least-one-use invariants (respectively) would be violated. Hence, we cannot allow linear and relevant values (which cannot be discarded) to be stored in unrestricted or affine references (which can be discarded). Considering yet another axis, we note that linear and affine references must be unique. Hence, we can free unique references, and also perform strong updates on them. Shared references, on the other hand, can never be deallocated and can only support weak updates. As we noted above, the rd operator induces an implicit copy while the wr operator induces an implicit drop. Therefore, whether we can read from or write to a reference depends entirely on the qualifier of its contents: rd is permitted if the contents are unrestricted or relevant (i.e., duplicable), wr is permitted if the contents are unrestricted or affine (i.e., discardable). The operation sw is permitted on any sort of reference, regardless of the qualifier of its contents. As noted above, strong writes and strong swaps, which change the type of the contents of the location, are only permitted on unique references. 7 2005/7/8 ∆ ι:κ ∆ τ: (RefPTy) ∆ ref τ : ∆; Γ e : τ q A ∆; Γ e : τ ∆ τ (New(U,A)) ∆; Γ newq e : qref τ ∆; Γ e : ξref τ ∆ A ξ (Free) ∆; Γ free e : τ A R q ∆; Γ e : τ (New(R,L)) ∆; Γ newq e : qref τ ∆; Γ e : ξref τ ∆ τ R (Read) ∆; Γ rd e : L(ξref τ τ ) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξref τ1 ∆ τ1 A ∆ A ξ (Write(Strong)) ∆; Γ2 e2 : τ2 ∆ τ2 ξ ∆; Γ wr e1 e2 : ξref τ2 ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξref τ1 ∆ A ξ (Swap(Strong)) ∆; Γ2 e2 : τ2 ∆ τ2 ∆; Γ sw e1 e2 : L(ξref τ2 ξ τ1) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξref τ ∆ τ (Write(Weak)) ∆; Γ2 e2 : τ ∆; Γ wr e1 e2 : ξref τ A ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξref τ (Swap(Weak)) ∆; Γ ∆; Γ2 e2 : τ sw e1 e2 : L(ξref τ τ) Figure 8. λrefURAL Static Semantics (Kinding and Typing Rules) Figure 8 gives the additional typing rules for λrefURAL. We note that the typing rules for core λURAL terms remain unchanged. There is no rule for locations, as locations are not allowed in the external language. Also note that the (New) and (Free) rules act as the introduction and elimination rules for ξref τ types, while the (Read), (Write), and (Swap) rules maintain an exactly-one-use invariant on references by consuming a value of type ξref τ1 and by producing a value of type ξref τ2 (possibly with τ1 = τ2). Finally, we note that wr may be encoded using an explicit sw and an implicit drop:4 ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξref τ ∆ τ A (Write(Weak)) ∆; Γ2 e2 : τ ∆; Γ wr e1 e2 : ξref τ d=ef let r, x = sw e1 e2 in // using (Swap(Weak)) // drop x, noting ∆ τ A r However, rd may not be encoded using an explicit sw and an implicit copy, as a suitable (discardable) dummy value cannot in general be synthesized. ∆; Γ e : ξref τ ∆ τ R (Read) ∆; Γ rd e : L(ξref τ τ ) d=ef let r, x = sw e ? in // where ∆; Γ // copy x, noting ∆ τ R ?:τ let r, y = sw r x in // using (Swap(Weak)) // drop y, but not necessarily ∆ τ A r, x 4. A Step-Indexed Model We prove the type soundness of λrefURAL in a manner similar to that employed by Appel’s Foundational PCC project [6]. The technique uses syntactic logical relations (that is, relations based on the operational semantics) where relations are further refined by an index that, intuitively, records the number of steps available for future evaluation. This stratification is essential for modeling the recursive functions (available via backpatching unrestricted references) and impredicative polymorphism present in the language. 4.1 Background: A Model of Unrestricted References Our model is based on the indexed model of ML-style references by Ahmed, Appel, and Virga [1, 4], henceforth AAV. In their model, the semantic interpretation T τ of a (closed) type τ is a set of triples of the form (k, Ψ, v), where, k is a natural number (called the approximation index or step index), Ψ is a (global) store typing that maps locations to (the interpretation of) their designated types, and v is a (closed) value. Intuitively, (k, Ψ, v) ∈ T τ says that in any 4 The encoding of a wr typed by the (Write(Strong)) rule makes use of the same term, but an alternate typing derivation. 8 2005/7/8 x }{{{ l1 L  l2 ????A?1 l3 U  l4 A  l5 A (a) (k, Ψ, Ω1, x) ∈ T τ1 y CCC3 Ö l 6 L l3 U  l4 A  l5 A (b) (k, Ψ, Ω2, y) ∈ T τ2 |xxx x, y FFF4 l1 L  l2 BBBBABB3 Ö l 6 L l3 U  l4 A  l5 A (c) Problem: Ω1 Ω2 = undefined Figure 9. Unique References in Shared References: Aliased or Owned? computation running for no more than k steps, v cannot be distinguished from values of type τ . Furthermore, since dereferencing a location consumes an execution step, in order to determine whether v has type τ for k steps it suffices to know the type of each store location for k − 1 steps; hence, Ψ need only specify each location’s type to approximation k −1. We use a similar indexing approach which is key to ensuring that our model is well-founded (as we shall demonstrate in Section 4.3). 4.2 Towards a Model of λrefURAL Aliasing and Ownership Though our model is similar to AAV, the presence of shared and unique references places very different demands on the model, which we illustrate by considering the interpretation of product types in various settings. In a language with only unrestricted references (e.g. AAV), one would say (k, Ψ, v1, v2 ) ∈ T τ1 τ2 if and only if (k, Ψ, v1) ∈ T τ1 and (k, Ψ, v2) ∈ T τ2 , where the store typing Ψ describes every location allocated by the program thus far. In this setting, every location (in Ψ) may be aliased; hence, the model allows v1 and v2 to point to data structures that overlap in the heap. In a language with only linear references [23, 2], however, one must ensure that the set of (linear) locations reachable from v1 is disjoint from the set of locations reachable from v2. This mirrors the fact that we can only construct tree-like data structures in this setting. Furthermore, it guarantees the safety of strong updates by providing a notion of exclusive ownership. Hence, to model a language with only linear references, it is useful to replace the global store description Ψ with a description of only the accessible (reachable) locations in the store, say Ω. Intuitively, when we write (k, Ω, v) ∈ T τ , we intend for Ω to describe only the subset of store locations that are accessible from, and hence, “owned” by v. Thus, one would say (k, Ω, v1, v2 ) ∈ T τ1 τ2 if and only if (k, Ω1, v1) ∈ T τ1 and (k, Ω2, v2) ∈ T τ2 , where the Ω is the disjoint union of Ω1 and Ω2. For the λrefURAL-calculus, we tried to build a model that supports both aliasing and ownership as follows. We defined the semantic interpretation of a type T τ as the set of tuples of the form (k, Ψ, Ω, v) where Ψ describes every U and R location allocated by the program and Ω describes only those A and L locations that are reachable from (and owned by) v. The interpretation of τ1 τ2 then naturally yields: (k, Ψ, Ω, v1, v2 ) ∈ T τ1 τ2 if and only if (k, Ψ, Ω1, v1) ∈ T τ1 and (k, Ψ, Ω2, v2) ∈ T τ2 , where the Ω is the disjoint union of Ω1 and Ω2. Unfortunately, the above model did not suffice for λrefURAL, since it assumes that every unique location reachable from v is exclusively owned by v, which is not the case when unique references may be stored in shared references. Unique References in Shared References: Aliased or Owned? Consider the situation depicted in Figure 9(a) where x maps to l1 and locations l1 through l5 are reachable from x. Locations “owned” by x are shaded. Notice that l1 and l2 are unique locations owned by x, while l4 and l5 are unique locations that x must consider aliased, since they can be reached (from other program subexpressions) via the unrestricted location l3. Figure 9(b) depicts such a subexpression, y. Note that y maps to l6 whose contents alias l3, making l4 and l5 reachable from y. 9 2005/7/8 In λrefURAL we may safely construct the pair x, y (shown in Figure 9(c)), but the interpretation of τ1 τ2 that we proposed above prohibits such a pair since locations l4 and l5 occur in both Ω1 and Ω2, violating the requirement that their domains be disjoint. To model the λrefURAL-calculus, we tried to further refine our model so that the interpretation of a type T τ is a set of tuples of the form (k, Ψ, Ω, Θ, v) where Ψ is as before, but now Ω describes unique owned locations, (i.e., those reachable from v without indirecting through a shared reference), while Θ describes unique aliased locations, (i.e., those that cannot be reached without indirecting through a shared cell). The intuition is that the interpretation of τ1 τ2 splits Ω into disjoint pieces for each component of the pair, but allows each component to use Ψ and Θ unchanged. This proposal, however, is fraught with complications. In particular, whether a unique location belongs in Ω or Θ depends on the configuration of the entire program, rather than just the type of the location. This limits the compositionality of the model. For instance, consider l5 in Figure 9(c). Clearly l5 must appear in Θ as it is reachable from an unrestricted location. However, if locations l1, l2, l3, and l6 did not exist, then l5 could appear in Ω. In the next section, we propose a far simpler solution that we consider one of the main technical contributions of our work. 4.3 A Model with Local Store Descriptions In our model of the λrefURAL-calculus, the semantic interpretation of a type T τ is a set of tuples of the form (k, q, ψ, v), where the local store description ψ describes only a part of the global store. Intuitively, ψ is the set of “beliefs” about the locations that appear as sub-expressions of the value v. Such locations are said to be directly accessible from the value v. Conversely, locations that are indirectly accessible from the value v are those locations that are reachable from v only by indirecting through one (or more) references. The local store description ψ says nothing about these indirectly-accessible locations. This enhances the compositionality of our model, making it straightforward to combine local store descriptions with one another. 4.3.1 Definitions We use the meta-variable χ to denote sets of tuples of the form (k, q, ψ, v) and the meta-variable ψ to denote partial maps from locations l to tuples of the form (q, χ).5 When χ corresponds to the semantic interpretation of a type and (k, q, ψ, v) ∈ χ, we intend that q is the qualifier of v, ψ is the local store description of v, and v is a closed value. When ψ corresponds to a local store description and ψ(l) = (q, χ), we intend that q is the qualifier of the reference and χ is the semantic interpretation of the type of its contents. Well-Founded & Well-Behaved Interpretations If we attempt to na¨ıvely construct a set-theoretic model based on these intentions, we are led to specify: Type = 2N×Quals×LocalStoreDesc×CValues LocalStoreDesc = Locs Quals × Type However, there is a problem with this specification: a simple diagonalization argument will show that the set Type of type interpretations has an inconsistent cardinality (i.e., it’s an ill-founded recursive definition). We can eliminate the inconsistency by stratifying our definitions, making essential use of the approximation index. To simplify the development, we first construct candidate sets, which are well-founded sets of our intended form. Next, we define some useful functions and predicates on these candidate sets. Finally, we construct our semantic interpretations by filtering the candidate sets, making use of the functions and predicates defined in the previous step. Our semantic interpretations impose a number of constraints (e.g., relating the qualifier of a reference to the qualifier of its contents) that are ignored in the construction of the candidate sets. Figure 10(b) defines our candidate sets by (strong) induction on k. Note that elements of CandAtomk are tuples with approximation index j strictly less than k. Hence, our definitions are well-defined at k = 0: CandAtom0 = ∅ CandUberType0 = {∅} CandLocalStoreDesc0 = Locs Quals × {∅} While our candidate sets establish the existence of sets of our intended form, our semantic interpretations will need to be well-behaved in other ways. There are key constraints associated with atoms, pre-types, types, and local store descriptions that will be enforced in our final definitions. Functions and predicates supporting these constraints are given in Figure 10(c). For any set χ, we define the k-approximation of the set (written χ k) as the subset of its elements whose indices are less than k; we extend the notion pointwise to local store descriptions ψ (written ψ k). Note that χ k and ψ k necessarily yield elements of CandUberTypek and CandLocalStoreDesck. 5 We write ψqual(l) and ψtype(l) for the respective projections of ψ(l). 10 2005/7/8 (a) PreType/Type Interpretation (Notation) χ ::= {(k, q, ψ, v), . . .} Local Store Description (Notation) ψ ::= {l → (q, χ), . . .} S(b) CandAtomk d=ef {(j, q, ψ, v) ∈ N × Quals × j><>>:ψ1 k ψ2 d=ef {l → ψ1 k(l) | l ∈ dom(ψ1) ∩ dom(ψ2)} {l → ψ1 k(l) | l ∈ dom(ψ1) \ dom(ψ2)} {l → ψ2 k(l) | l ∈ dom(ψ2) \ dom(ψ1)} if ∀l ∈ dom(ψ1) ∩ dom(ψ2). ψ1 k(l) = ψ2 k(l) and ∀l ∈ dom(ψ1). A ψ1qual(l) ⇒ l ∈/ dom(ψ2) and ∀l ∈ dom(ψ2). A ψ2qual(l) ⇒ l ∈/ dom(ψ1) undefined otherwise Figure 13. λrefURAL Model (Join Partial Function) Clearly, if ψ1 and ψ2 have disjoint sets of beliefs about the store, then ψ1 k ψ2 is defined and equal to the union of their beliefs: (k, q1, ψ1 = {l1 → (q1, T τ1 )}, l1) ∈ T q1 ref τ1 (k, q2, ψ2 = {l2 → (q2, T τ2 )}, l2) ∈ T q2 ref τ2 Jψ1 _ _ _ _ _ _ _ ? _l1 _→_(q1_, T_ τ_1 )_ ψ2 ?? _ _ _ _ _ _ _ ?? _l2 _→_(q2_, T_ τ_2 )_ ? ψ1 ψ2 _ _ _ _ _ _ _ = _ _ _ ? _ _ _ _ _l1 _→_(q1_, T_ τ_1 )_ _l2 _→_(q2_, T_ τ_2 )_ ? In the more general case, where the same location may be found in the domain of both ψ1 and ψ2, there are two requirements enforced by the definition of ψ1 k ψ2. First, we require that for any location l that is described by both ψ1 and ψ2, it must be the case that ψ1 and ψ2 have identical beliefs about l to approximation k. Note that ψ1 and ψ2 must agree on both the qualifier of the location as well as the type of the location’s contents: (k, U, ψ1 = {l → (U, T τ )}, l) ∈ T Uref τ (k, U, ψ2 = {l → (R, T τ )}, l) ∈ T Rref τ Jψ1 _ _ _ _ _ _ ? _l →_ (_U, _T _τ )_ ψ1 _ _ _ _ _ _ ψ1 _ ψ_1 _ _ _ _ ? _l →_ (_U, _T _τ )_ = ? _l →_ (_U, _T _τ )_ ?? ?? ?? Jψ1 _ _ _ _ _ _ ? _l →_ (_U, _T _τ )_ ψ2 _ _ _ _ _ _ ? _l →_ (_R, T_ τ_ )_ = ?? ?? undefined The second requirement is more subtle, having to do with the notion of directly-accessible locations. Suppose that l3 is a linear or affine location mapped by ψb. Therefore, a value vb with local store description ψb must contain l3 as a sub-expression. Since l3 is linear or affine, this occurrence of l3 in the value vb must be the one (and only) occurrence of l3 in the entire program state. Now, suppose that l3 is also in the domain of a local store description ψc. As before, a value vc with local store description ψc must contain l3 as a sub-expression. If we were to attempt to form the value vb, vc , then 13 2005/7/8 we would have a value with two distinct occurrences of l3, violating the uniqueness of the location l3. Hence, we consider ψb and ψc to represent incompatible (contradictory) beliefs about the current store: (k, L, ψa = {l1 → (U, T τ1 ), l2 → (L, T τ2 ), va = l1, l2 ) ∈ T L(Uref τ1 (k, L, ψb = {l1 → (U, T τ1 ), l3 → (L, T τ3 ), vb = l1, l3 ) ∈ T L(Uref τ1 (k, L, ψc = {l3 → (L, T τ3 ), vc = l3, ) ∈ T L(Lref τ3 U1 ) Lref τ2) Lref τ3) Jψa _ _ _ _ _ _ _ _ ? __ _ _ _l1 _→ (_U, T_ τ_1 )_ ψb _ _ _ _ _ _ ψa ψb _ _ _ _ _ _ ? __l1 _→_ (__U, _T_ τ__1 )__ = _ _ ? __ _ _ __l1 _→_ (__U, _T_ τ__1 )__ _l2 _→ (_L, T_ τ_2 )_ ? ? _l3 _→ (_L, T_ τ_3 )_ _l2 _→ (_L, T_ τ_2 )_ _l3 _→ (_L, T_ τ_3 )_ Jψb _ _ _ _ _ _ ? __l1 _→_ (__U, _T_ τ__1 )__ ψc ?? _ _ _ _ _ _ = ? _l3 _→ (_L, T_ τ_3 )_ ? _l3 _→ (_L, T_ τ_3 )_ undefined Functions & Abstractions: Closure Location Beliefs Since functions and abstractions are suspended computations, their interpretations are given in terms of the interpretation of types as computations (see below). A function λx. e with qualifier qc and local store description ψc (where ψc describes the locations directly accessible from the function’s closure and, hence, must satisfy P(qc, ψc)) is in the interpretation of τ1 τ2 for k steps if, at some point in the future, when there are j < k steps left to execute, and there is an argument va such that (j, , ψa, va) ∈ T τ1 and the beliefs ψc and ψa are compatible, then e[va/x] looks like a computation of type τ2 for j steps. The interpretation of ∀α:κ. τ is analogous, except that we quantify over (type-level term) interpretations I ∈ K κ . Store Satisfaction: Tracing Location Beliefs The interpretation of types as computations (Comp) makes use of an auxiliary relation s :k ψ (given in Figure 14), which says that the store s satisfies local store description ψ (to approximation k). We motivate the definition of s :k ψ by drawing an analogy with the specification of a tracing garbage collector (see Figure 15). As described above, ψ corresponds to (beliefs about) the portion of the store directly accessible from a value (or multiple values, when ψ corresponds to k-ed store descriptions). Hence, we can consider dom(ψ) as a set of root locations. In the definition of s :k ψ, S corresponds to the set of reachable (root and non-root) locations in the store that would be discovered by the garbage collector. The function Fψ maps each location in S to a local store description, while the function Fq maps each location to a qualifier. It is our intention that, for each location l, Fq(l) is an appropriate qualifier and Fψ(l) is an appropriate local store description for the value sval(l). Hence, we can consider dom(Fψ(l)) as the set of child locations traced from the contents of l. Having chosen the set S and the functions Fψ and Fq, we require that they satisfy three criteria. The congruity criteria ensures that our choices are both internally consistent and consistent with the store s. The “global” store description ψ∗ combines the local store descriptions of the roots with the local store descriptions of the contents of every reachable location; the implicit requirement that ψ∗ is defined ensures that the local beliefs of the roots and individual store contents are all compatible. The clause dom(ψ∗) = S requires that S and Fψ are chosen such that S includes all the reachable locations (and not just some of the reachable locations), while the clause dom(s) ⊇ S requires that all of the reachable locations are actually in the store. Finally, (j, Fq, Fψ(l) j, sval(l)) ∈ ψ∗type(l) k ensures that the contents of l, with the qualifier assigned by Fq and local store description assigned by Fψ, is in the type assigned by the global store description ψ∗ (for j < k steps). The minimality criteria ensures that our choice for the set S does not contain any locations not reachable from the roots. For example, in Figure 15, including l11 in S would not violate congruity, but would violate minimality. Finally, the reachability criteria ensures that every linear and relevant location is reachable from the roots (and, hence, has not been implicitly discarded). Computations: Relating Current to Future Beliefs Informally, the interpretation of types as computations Comp(k, ψs, es, χ) (see Figure 11) says that if the expression es (with beliefs ψs, again, corresponding to the locations appearing as sub-expressions of es) reaches an irreducible state in less than k steps, then it must have reduced to a value vf (with beliefs ψf ) that belongs to the type interpretation χ. More precisely, we pick a starting store ss such that ss :k (ψs k ψr), where ψr is the set of beliefs about the store held by the rest of the computation (alternatively, the set of beliefs held by es’s continuation). If (ss, es) steps to an irreducible configuration (sf , ef ) in j < k steps, then the following conditions hold. First, ef must be a value with a qualifier qf and a set of beliefs ψf such that (k − j, qf , ψf , ef ) ∈ χ. Second, the following two sets of beliefs must be compatible: ψf (what ef believes) and ψr (what the rest of the computation believes — note that these beliefs remain unchanged). Third, the final store sf must satisfy the combined set of these beliefs. 14 2005/7/8 s :k ψ d=ef ∃S : 2Locs . ∃Fψ : S → LocalStoreDesc. J∃Fq : S → Quals. let ψ∗ = (ψ k l∈S k Fψ (l)) in dom(ψ∗) = S ∧ dom(s) ⊇ S ∧ ∀l ∈ S. ∀j < k. (j, Fq(l), Fψ(l) j , sval(l)) ∈ ψ∗type(l) k ∧ squal(l) = ψ∗type(l) ∧ ∀S† ⊆ S. dom(ψ) ⊆ S† ∧ (∀l ∈ S†. dom(Fψ(l)) ⊆ S†) ⇒ S = S† ∧ ∀l ∈ dom(s). R squal(l) ⇒ l ∈ S 9>>= >>; congruity   minimality reachability Figure 14. λrefURAL Model (Store Satisfaction) s l0 → (q0, v0) G GF l4 → (q4, v4) GF G l7 → (q7, v7) BC l1 → (q1, v1)  BC l5 → (q5, v5)  l8 → (q8, v8) l2 → (q2, v2) GF  l3 → (q3, v3) BC GF G l9 → (q9… , v9) BC G l6 → (q6, v6) ! l10 → (q10, v10) l11 → (q11, v11) ψ_ _ _ _ _ _ _ _l0 _→_(q0_, T_ τ_0 )_ l12 → (q1… 2, v12) l13 → (q13, v13) _ _ _ _ _ _ _ _l1 _→_(q1_, T_ τ_1 )_ : _ _ _ _ _ _ _ _l2 _→_(q2_, T_ τ_2 )_ ! l14 → (q14, v14) _ _ _ _ _ _ _ _l3 _→_(q3_, T_ τ_3 )_ ? ? ? ? ? ? ? ? s_: ψ_ _ _ _ _ _ _ _l0 _→ _(q0_, v0_: T_ τ_0 )_ GF G__l4 _ _→ ___ _(q4_, v4_: _ T_ _ τ_4 _ )_ GF G__l7 _ _→ ___ _(q7_, v7_: _ T_ _ τ_7 _ )_ _ _ _ _ _ _ _ _B C _ _ _ _  _ _ _ _B C _l1 _→ _(q1_, v1_: T_ τ_1 )_ _l5 _→ _(q5_, v5_: T_ τ_5 )_ _ _ _ _  _ _ _ _ _l8 _→ _(q8_, v8_: T_ τ_8 )_ l11 → (q11, v11) l12 → (q1… 2, v12) _ _ _ _ _ _ _ _ ≡ _l2 _→ _(q2_, v2_: T_ τ_2 )_ GF _ _ _ _  _ _ _ _ | {z }_l3 _→ _(q3_, v3_: T_ τ_3 )_ | {zdom(ψ) dom(ψ∗) = S where Fψ(l1) _ _ _ _ _ _ _ ? _l4 _→_(q4_, T_ τ_4 )_ BC GF G__l9 _ _→ ___ _(q9_, v9_… : _ T_ _ τ_9 _ )_ G__l6 _ _→ ___ _(q6_, v6_: _ T_ _ τ_6 _B C )_ _ _ _ _ _! _ _ _ _ _ _l10_→_ (q_10_, v1_0 :_T _τ1_0 )_ } l13 → (q13, v13) ! l14 → (v14, v14) Fψ (l5 ) ?? ? _ _ _ _ _ _ _ ? _l7 _→_(q7_, T_ τ_7 )_ ? ? ? ? ? ? ? ?? ? ? ? ? etc. ? ? ?? ? ? ? ? _ _ _ _ _ _ _ ? ? ? ? _l3 _→_(q3_, T_ τ_3 )_ ? ? ? Figure 15. s : ψ Example 15 2005/7/8 D • = {∅} D ∆, α:κ = {δ[α → I] | δ ∈ D ∆ ∧ I ∈ K κ } G ∆ • δ = {(k, q, {}, ∅)} G ∆ Γ, x:τ δ = {(k, q, ψ, γ[x → v]) | ψ = (ψΓ k ψx) ∧ (k, qΓ, ψΓ, γ) ∈ G ∆ Γ δ ∧ qΓ q ∧ (k, qx, ψx, v) ∈ T ∆ τ : δ ∧ qx q} ∆; Γ e : τ d=ef ∀k ≥ 0. ∀δ, qΓ, ψΓ, γ. δ ∈ D ∆ ∧ (k, qΓ, ψΓ, γ) ∈ G ∆ Γ δ ⇒ Comp(k, ψΓ, γ(e), T ∆ τ : δ) Figure 16. λrefURAL Model (Additional Interpretations) Note that since ψr is an arbitrary set of beliefs compatible with ψs, one instantiation of ψr is the local store description that includes all of the shared locations of ψs. By requiring that ψf and sf are compatible with ψr, we ensure that the types and qualifiers and allocation status of shared locations are preserved. Judgements: Type Soundness Finally, the semantic interpretation of a typing judgement ∆; Γ e : τ (see Figure 16) asserts that for all k ≥ 0, if δ is a mapping from type-level variables to an element of the appropriate kind interpretation, and γ is a mapping from variables to closed values, and ψΓ is a local store description for the values in the range of γ, then (k, ψΓ, γ(e)) is in the interpretation of τ as a computation (Comp(k, ψΓ, γ(e), T τ )). The appendicies give the proof of the following theorem which shows the soundness of the λrefURAL typing rules with respect to the model. THEOREM 1. (λrefURAL Soundness) If ∆; Γ e : τ , then ∆; Γ e : τ . An immediate corollary is type-safety of λrefURAL. Another interesting corollary is that if we evaluate a closed, welltyped term of base type (e.g., q1 ) to a value, then the resulting store will have no linear or relevant references. COROLLARY 2. (λrefURAL Safety) If •; • e1 : τ and ({}, e1) −→∗ (s2, e2), then either ∃v2. e2 ≡ v2 or ∃s3, e3. (s2, e2) −→ (s3, e3). COROLLARY 3. (λrefURAL Collection) If •; • e1 : q1 and ({}, e1) −→∗ (s2, v2), then ∀l ∈ dom(s2). sq2ual(l) A. Proof (λrefURAL Safety) Suppose •; • e1 : τ and ({}, e1) −→∗ (s2, e2). If ¬irred (s2, e2), then ∃s3, e3. (s2, e2) −→ (s3, e3). If irred (s2, e2), then ∃i. ({}, e1) −→i (s2, e2). Theorem 1 applied to •; • e1 : τ yields •; • e1 : τ . •; • e1 : τ instantiated with i + 1 ≥ 0, ∅ ∈ D • , and (i + 1, U, {}, ∅) ∈ G • ∅ yields Comp(i + 1, {}, e1, T • τ : ∅). Comp(i + 1, {}, e1, T • τ : ∅) instantiated with i < i + 1, s1 :i+1 ({} i+1 {}), ({}, e1) −→i (s2, e2), and irred (s2, e2) yields q2 and ψ2 such that s2 :1 (ψ2 1 {}) and (1, q2, ψ2, e2) ∈ T • τ : ∅. Recall that T • τ : ∅ ∈ Type and Type ⊆ CandUberTypeω = 2CandAtomω . Hence, (1, q2, ψ2, e2) ∈ CandAtomω = k≥0 CandAtomk, which implies that e2 ∈ CValues and ∃v2. e2 ≡ v2. Proof (λrefURAL Collection) Suppose •; • e1 : q1 and ({}, e1) −→∗ (s2, v2). By the reasoning above, (1, q2, ψ2, v2) ∈ T • q1 : ∅, which implies that q2 = q, ψ2 = {}, and v2 = Recall that s2 :1 ({} 1 {}) ≡ s2 :1 {} ≡ ∃S, Fψ, Fq. . . .. The minimality criteria of s2 :1 {} instantiated with ∅ ⊆ S, dom({}) ⊆ ∅, and (∀l ∈ ∅. dom(Fψ(l)) ⊆ ∅) yields S = ∅. . 16 2005/7/8 The reachability criteria of s2 :1 {} yields ∀l ∈ dom(s2). R sq2ual(l) ⇒ l ∈ ∅, which implies ∀l ∈ dom(s2). sq2ual(l) A. 4.4 Discussion A key difference in the model presented here, as compared to previous models of mutable state, is the localization of the store description. Recall that we identify the local store description of a value with those locations that are directly accessible from the value. This is in contrast to the AAV model of unrestricted references [1, 4], where the global store description of any value describes every location that has been allocated. It is also in contrast to our previous model of linear references [23, 2], where the store description of a value describes the reachable locations from that value. The transition from a global store description to a local store description is motivated by the insight that storing a unique object in a shared reference “hides” the unique object in some way. Note that the shared reference must mediate all access to the unique object. The authors have found it hard to construct a model where the store description of a value (in the interpretation of a type) describes the entire store or even the store reachable from the value. When one attempts to describe the entire store, there is a difficulty identifying where the “real” occurrence of a unique location is to be found. When one attempts to describe the reachable store, there is a difficulty defining the relation; it cannot be defined point- wise, and one is required to formally introduce the notions of directly- and indirectly-accessible locations. Furthermore, the reachable store is a property of the actual store, not of the type; hence, it seems better to confine reachability to the store satisfaction relation. We further note that the model of mutable references given in this paper subsumes the models of mutable references cited above. Hence, the technique of localizing the store description subsumes the techniques used by previous approaches. Although our model of substructural references is different from the previous model of unrestricted references, our model retains the spirit of the step-indexed approach used in Foundational PCC [6, 7] and may be applicable in future extensions of FPCC. This approach, in which the model mixes denotational and operational semantics, offers a number of distinct advantages over a purely syntactic approach to type soundness. One obvious advantage of this approach is that it gives rise to a simpler set of typing rules; note that our typing judgement requires neither a store description component nor a rule for locations. A less obvious advantage of this approach is that it gives rise to stronger meta- theoretic results. For example, the impredicative polymorphism of λrefURAL implies a strong parametricity theorem: an element of T ∀α: . τ behaves uniformly on all elements of Type, which includes elements that do not correspond to the interpretation of any syntactic type. This approach also naturally extends to union and intersection types and to an inclusion interpretation of subtyping. Finally, a (well-founded) set-theoretic model means that soundness and safety proofs are amenable to formalization in the higher-order logic of FPCC. While we are partial to the step-indexed approach, we acknowledge that there is no fundamental difficulty in adopting a purely syntactic approach to proving the type soundness of substructural state. However, we believe that any proof of type soundness must adopt many of the insights presented here. For example, we conjecture that the typing rule for well-typed configurations would naturally take the form: Kl∈S ψ∗ = ψ Fψ (l) dom(ψ∗) = S dom(s) ⊇ S ∀l ∈ S. ·; ·; Fψ(l) sval(l) : ψ∗type(l) ∧ squal(l) = ψ∗qual(l) s:ψ ·; ·; ψ e : τ (s, e) : τ Note that the judgement s : ψ mirrors the store satisfaction predicate given in Figure 14. The store typing component complicates the judgement ∆; Γ; ψ e : τ , which must further rely upon an operator ψ1 ψ2 = ψ to split the locations in ψ between the store typings ψ1 and ψ2. Splitting the store typing is necessary to ensure that a given unique location is used by at most one sub-expression. The operator in the syntactic approach would need to satisfy many of the same properties as the k operator in the step-indexed approach (e.g., identical beliefs about locations in the common domain and no unique locations in the common domain). 5. Related Work Our λURAL is most directly influenced by the presentation of substructural type systems by Walker [30], which in turn draws upon the work of Wansbrough and Peyton-Jones [33] and Walker and Watkins [32]. Relative to that work, we have added both relevant and affine qualifiers, which is necessary to account for the varied forms of linearity found in higher-level programming-language proposals. 17 2005/7/8 A related body of work is that on type systems used to track resource usage [28, 22, 33, 21, 16, 19]. We note that the usage subsumption found in these systems (e.g., a “possibly used many times” variable may be subsumed to appear in a context requiring a “used exactly once” value) is not applicable in our setting (e.g., it is clearly unsound to subsume Uref τ to Lref τ ), due to differences in the interpretation of type qualifiers. Section 1 noted a number of projects that have introduced some form of linearity to “tame” state. An underlying theme is that linearity and strong updates can be used to provide more effective memory management (c.f. [10, 18, 9, 8]). More recent research has explored other ways in which unique and shared data may be mixed. For example, Cyclone’s alias construct [17] takes a unique pointer and returns a shared pointer to the same object, which is available for a limited lexical scope. Vault’s focus and CQuals’s restrict constructs [14, 5] provide the opposite behavior: temporarily giving a linear view of an object of shared type. Both behaviors are of great practical significance. Our model’s semantic interpretations seem strongly related to the logic of Bunched Implications (BI) [20] and Reynolds’ separation logic [25]. In particular, our interpretation of and resemble the resource semantics for the ∗ and −∗ connectives in BI. Finally, Boyland and Retert have recently proved the soundness of a variation of Vault by giving an operational semantics of “adoption” [11]. The authors note that adoption may be used to embed a unique pointer within another object; their notion of uniqueness most closely resembles our affine references, as access keys may be dropped. 6. Conclusion and Future Work We have presented the λrefURAL-calculus, a substructural polymorphic λ-calculus with mutable references of unrestricted, relevant, affine, and linear sorts. We motivated the design decisions, gave a type system, and constructed a step-indexed model of λrefURAL, where types are interpreted as sets of store description / value pairs, which are further refined using an index representing the number of steps available for future evaluation. In previous work [23, 2], we separated the typing components of a mutable object into two pieces: an unrestricted pointer to the object and a linear capability for accessing the contents of the object. We believe that we can extend the current language and model in the same way. The advantage of this approach is that separating the name of a reference from what it currently holds gives us a model of alias types [27, 31]. As noted in the previous section, allowing a unique pointer to be temporarily treated as shared (and vice versa) can be useful in practice. Understanding how to model these advanced features is a long-term goal of this research. A promising aproach is to model regions as a linear capability to access objects in the region and allow changes in reference qualifiers to be mediated by this capability. Acknowledgments We would like to thank Dan Grossman, Aleks Nanevski, and Dan Wang for their helpful comments. References [1] Amal Ahmed, Andrew W. Appel, and Roberto Virga. An indexed model of impredicative polymorphism and mutable references. Available at http://www.cs.princeton.edu/~appel/papers/impred.pdf, January 2003. [2] Amal Ahmed, Matthew Fluet, and Greg Morrisett. L3: A linear language with locations. Technical Report TR-24-04, Harvard University, October 2004. [3] Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. Technical Report TR-16-05, Harvard University, July 2005. [4] Amal Jamil Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. [5] Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi. Checking and inferring local non-aliasing. In Proc. Programming Language Design and Implementation (PLDI), pages 129–140, June 2003. [6] Andrew W. Appel. Foundational proof-carrying code. In Proc. Logic in Computer Science (LICS), pages 247–258, June 2001. [7] Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657–683, September 2001. [8] David Aspinall and Adriana Compagnoni. Heap bounded assembly language. Journal of Automated Reasoning, 31:261–302, 2003. [9] David Aspinall and Martin Hofmann. Another type system for in-place update. In Proc. European Symposium on Programming (ESOP), pages 36–52, March 2002. [10] Henry Baker. Lively linear LISP—look ma, no garbage. ACM SIGPLAN Notices, 27(8):89–98, 1992. [11] John Tang Boyland and William Retert. Connecting effects and uniqueness with adoption. In Proc. Principles of Programming Languages (POPL), pages 283–295, January 2005. 18 2005/7/8 [12] James Cheney and Greg Morrisett. A linearly typed assembly language. Technical Report 2003-1900, Department of Computer Science, Cornell University, 2003. [13] Robert DeLine and Manuel Fa¨hndrich. Enforcing high-level protocols in low-level software. In Proc. Programming Language Design and Implementation (PLDI), pages 59–69, June 2001. [14] Manuel Fa¨hndrich and Robert DeLine. Adoption and focus: Practical linear types for imperative programming. In Proc. Programming Language Design and Implementation (PLDI), pages 13–24, June 2002. [15] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987. [16] Jo¨rgen Gustavsson and Josef Svenningsson. A usage analysis with bounded usage polymorphism and subtyping. In Proc. International Workshop on Implementation of Functional Languages (IFL), pages 140–157, September 2001. [17] Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Experience with safe manual memory-management in Cyclone. In Proc. International Symposium on Memory Management (ISMM), pages 73–84, October 2004. [18] Martin Hofmann. A type system for bounded space and functional in-place update. In Proc. European Symposium on Programming (ESOP), pages 165–179, March 2000. [19] Atsushi Igarashi and Naoki Kobayashi. Resource usage analysis. In Proc. ACM Principles of Programming Languages (POPL), pages 331–342, January 2002. [20] Samin Ishtiaq and Peter O’Hearn. BI as an assertion language for mutable data structures. In Proc. Principles of Programming Languages (POPL), pages 14–26, January 2001. [21] Naoki Kobayashi. Quasi-linear types. In Proc. Principles of Programming Languages (POPL), pages 29–42, January 1999. [22] Torben Æ. Mogensen. Types for 0, 1 or many uses. In Proc. International Workshop on Implementation of Functional Languages (IFL), pages 112–122, 1998. [23] Greg Morrisett, Amal Ahmed, and Matthew Fluet. L3: A linear language with locations. In Proc. International Conference on Typed Lambda Calculi and Applications (TLCA), pages 293–307, April 2005. [24] Peter W. O’Hearn and John C. Reynolds. From Algol to polymorphic linear lambda-calculus. Journal of the ACM, 47(1):167–223, 2000. [25] John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Logic in Computer Science (LICS), pages 55–74, July 2002. [26] Sjaak Smetsers, Erik Barendsen, Marko C. J. D. van Eekelen, and Rinus J. Plasmeijer. Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. In Dagstuhl Seminar on Graph Transformations in Computer Science, volume 776 of Lecture Notes in Computer Science, pages 358–379. Springer-Verlag, 1994. [27] Fred Smith, David Walker, and Greg Morrisett. Alias types. In Proc. European Symposium on Programming (ESOP), pages 366–381, March 2000. [28] David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In Proc. Functional Programming Languages and Computer Architecture (FPCA), pages 1–11, June 1995. [29] Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, April 1990. IFIP TC 2 Working Conference. [30] David Walker. Substructural type systems. In Benjamin Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 1, pages 3–43. MIT Press, Cambridge, MA, 2005. [31] David Walker and Greg Morrisett. Alias types for recursive data structures. In Proc. Workshop on Types in Compilation (TIC), pages 177–206, September 2000. [32] David Walker and Kevin Watkins. On regions and linear types. In Proc. International Conference on Functional Programming (ICFP), pages 181–192, September 2001. [33] Keith Wansbrough and Simon Peyton-Jones. Once upon a polymorphic type. In Proc. Principles of Programming Languages (POPL), pages 15–28, January 1999. 19 2005/7/8 Appendix: Formal Development The following appendices present a formal development of the language, step-indexed model, and soundness proof described in the main body of this technical report. Previous research has suggested that linearity and, by extension, the other substructural sorts have been and will continue to be a powerful means of “taming” state and effects in programming languages and type systems. With this in mind, we propose a framework comprised of a core substructural polymorphic λ-calculus and type system, stepindexed model, and proof of soundness. The entire development of this core language is done with respect to an abstract global stateful world, additional abstract expression forms that interact with the world, and abstract world descriptions, which impart semantic meaning to worlds. Having held these components abstract, the proof establishing the soundness of our step-indexed model is itself parameterized by a collection of requirements that must satisfied by these abstract components. Hence, our methodology is to instantiate the framework by choosing concrete worlds, expression forms, and world descriptions, showing that these concrete components meet the requirements, and discharge any additional proof cases introduced by the new components. In Appendix A, we use shaded boxes to indicated abstracted components, requirements, and proof cases that depend upon the particular concrete instantiation. In Appendix B, we show a simple instantiation that adds recursive types to the core language. In Appendix C, we show the instantiation for mutable references. 20 2005/7/8 A Core Language A.1 Syntax Kind Level: Kinds Extended Kinds κ ::= QUAL | PRETYPE | TYPE | κX κX ::= . . . Type Level: Constant Qualifiers Qualifiers PreTypes Extended PreTypes Types Terms Extended Terms q ∈ Quals = {U, R, A, L}  L ?? A ??  R U ξ ::= α | q τ ::= α | τ1 τ2 | 1 | τ1 τ2 | 1 | τ1 τ2 | 0 | τ1 τ2 | ∀α:κ. τ | ∃α:κ. τ | τ X τ X ::= . . . τ ::= α | ξτ ι ::= ξ | τ | τ | ιX ιX ::= . . . Expression Level: Values v ::= x | λx. e | | v1, v2 | | e1, e2 | inl v1 | inr v2 | Λ. e | v | vX Extended Values vX ::= . . . Expressions e ::= v | e1 e2 | let = e1 in e2 | let x1, x2 = e1 in e2 | fst e | snd e | abort e | case e of inl x1 ⇒ e1 inr x2 ⇒ e2 | e [] | let x = e1 in e2 | copy e | drop e | eX Extended Expressions eX ::= . . . Figure 1: Core Language – Syntax 21 A.2 Operational Semantics World w ::= . . . Evaluation Contexts E ::= [ ] | E e2 | v1 E2 | let = E in e2 | let x1, x2 = E in e2 | fst E | snd E abort E | case E of inl x1 ⇒ e1 inr x2 ⇒ e2 E [] | let x = E in e2 | copy E | drop E | EX Extended Evaluation Contexts EX ::= . . . (app) (let-munit) (let-mpair) (fst) (snd) (case-inl) (case-inr) (inst) (let-pack) (copy) (drop) (extended) (ctxt) (w, (λx. e) v) −→ (w, let = in e) −→ (w, let x1, x2 = v1, v2 in e) −→ (w, fst e1, e2 ) −→ (w, snd e1, e2 ) −→ (w, case inl v of inl x1 ⇒ e1 inr x2 ⇒ e2) −→ (w, case inr v of inl x1 ⇒ e1 inr x2 ⇒ e2) −→ (w, (Λ. e) []) −→ (w, let x = v in e) −→ (w, copy v) −→ (w, drop v) −→ ... (w, e) −→ (w , e ) (w, E[e]) −→ (w , E[e ]) (w, e[v/x]) (w, e) (w, e[v1/x1][v2/x2]) (w, e1) (w, e2) (w, e1[v/x1]) (w, e2[v/x2]) (w, e) (w, e[v/x]) (w, v, v ) (w, ) Figure 2: Core Language – Operational Semantics 22 A.3 Static Semantics ∆ ι:κ Term Context ∆ ::= • | ∆, α:κ (VarKn) α:κ ∈ ∆ ∆ α:κ (Qual) ∆ q : QUAL (FnPTy) ∆ τ1 : TYPE ∆ τ2 : TYPE ∆ τ1 τ2 : PRETYPE (MUnitPTy) ∆ 1 : PRETYPE (MPairPTy) ∆ τ1 : TYPE ∆ τ2 : TYPE ∆ τ1 τ2 : PRETYPE (AUnitPTy) ∆ 1 : PRETYPE (APairPTy) ∆ τ1 : TYPE ∆ τ2 : TYPE ∆ τ1 τ2 : PRETYPE (VoidPTy) ∆ 0 : PRETYPE (SumPTy) ∆ τ1 : TYPE ∆ τ2 : TYPE ∆ τ1 τ2 : PRETYPE (AllPTy) ∆, α:κ τ : TYPE ∆ ∀α:κ. τ : PRETYPE (ExPTy) ∆, α:κ τ : TYPE ∆ ∃α:κ. τ : PRETYPE (UserPTy) . . . (Type) ∆ ξ : QUAL ∆ τ : PRETYPE ∆ ξτ : TYPE (UserTerm) . . . Figure 3: Core Language – Static Semantics (I) 23 ∆Γ Value Context Γ ::= • | Γ, x:τ ∆• ∆ Γ ∆ τ : TYPE ∆ Γ, x:τ Figure 4: Core Language – Static Semantics (II) ∆ ξ1 ξ2 ∆τ ξ ∆Γ ξ ∆ ξ2 : QUAL ∆ U ξ2 ∆ ξ : QUAL ∆ξ ξ q1 q2 ∆ q1 q2 ∆ ξ1 : QUAL ∆ ξ1 L ∆ ξ1 ξ ∆ξ ∆ ξ1 ξ2 ξ2 ∆ τ : TYPE ∆τ L ∆ τ : PRETYPE ∆ ξ ∆ ξτ ξ ξ ∆ ξ : QUAL ∆• ξ ∆Γ ξ ∆τ ξ ∆ Γ, x:τ Figure 5: Core Language – Static Semantics (III) ∆ Γ ; Γ1 Γ2 ∆ •;• • ∆ Γ ; Γ1 Γ2 ∆ τ : TYPE ∆ Γ, x:τ ; Γ1, x:τ Γ2 ∆ Γ ; Γ1 Γ2 ∆ τ : TYPE ∆ Γ, x:τ ; Γ1 Γ2, x:τ ∆ Γ ; Γ1 Γ2 ∆ τ R ∆ Γ, x:τ ; Γ1, x:τ Γ2, x:τ Figure 6: Core Language – Static Semantics (IV) 24 ∆; Γ e : τ (Var) ∆ τ : TYPE ∆; •, x:τ x : τ (Fn) ∆ ξ : QUAL ∆ Γ ξ ∆; Γ λx. e : ξ(τ1 ∆; Γ, x:τ1 τ2) e : τ2 (MUnit) ∆ ξ : QUAL ∆; • : ξ1 (MPair) ∆ Γ ; Γ1 Γ2 ∆ ξ : QUAL ∆; Γ1 v1 : τ1 ∆ τ1 ∆; Γ v1, v2 : ξ(τ1 τ2) ξ ∆; Γ2 v2 : τ2 ∆ τ2 ξ (AUnit) ∆ ξ : QUAL ∆; Γ ∆Γ : ξ1 ξ (APair) ∆ ξ : QUAL ∆ Γ ξ ∆; Γ e1 : τ1 ∆; Γ e1, e2 : ξ(τ1 τ2) ∆; Γ e2 : τ2 (Inl) ∆ ξ : QUAL ∆; Γ v : τ1 ∆ τ1 ξ ∆; Γ inl v : ξ(τ1 τ2) ∆ τ2 : TYPE (Inr) ∆ ξ : QUAL ∆ τ1 : TYPE ∆; Γ v : τ2 ∆; Γ inr v : ξ(τ1 τ2) ∆ τ2 ξ (All) ∆ ξ : QUAL ∆ Γ ξ ∆, α:κ; Γ ∆; Γ Λ. e : ξ∀α:κ. τ e:τ (Pack) ∆ ξ : QUAL ∆ ι : κ ∆; Γ v : τ [ι/α] ∆; Γ v : ξ∃α:κ. τ ∆ τ [ι/α] ξ (UserVal). . . Figure 7: Core Language – Static Semantics (Va) 25 ∆; Γ e : τ (App) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξ(τ1 τ2) ∆; Γ e1 e2 : τ2 ∆; Γ2 e2 : τ1 (Let-MUnit) ∆ Γ ; Γ1 Γ2 ∆; Γ ∆; Γ1 e1 : ξ1 ∆; Γ2 let = e1 in e2 : τ e2 : τ (Let-MPair) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξ(τ1 τ2) ∆; Γ2, x1:τ1, x2:τ2 ∆; Γ let x1, x2 = e1 in e2 : τ e2 : τ (Fst) ∆; Γ e : ξ(τ1 τ2) ∆; Γ fst e : τ1 (Snd) ∆; Γ e : ξ(τ1 τ2) ∆; Γ snd e : τ2 (Abort) ∆; Γ e : ξ0 ∆ τ : TYPE ∆; Γ abort e : τ (Case) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e : ξ(τ1 τ2) ∆; Γ2, x1:τ1 : e1 : τ ∆; Γ2, x2:τ2 : e2 : τ ∆; Γ case e of inl x1 ⇒ e1 inr x2 ⇒ e2 : τ (Inst) ∆; Γ e : ξ∀α:κ. τ ∆ ∆; Γ e [] : τ [ι/α] ι:κ (Let-Pack) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e1 : ξ∃α:κ. τ1 ∆ Γ2 ∆ τ2 : TYPE ∆; Γ let x = e1 in e2 : τ2 ∆, α:κ; Γ2, x:τ1 e2 : τ2 (Copy) ∆; Γ e : τ ∆ τ R ∆; Γ copy e : L(τ τ ) (Drop) ∆; Γ e : τ ∆ τ ∆; Γ drop e : L1 A (Weak) ∆ Γ ; Γ1 Γ2 ∆; Γ1 e : τ ∆; Γ e : τ ∆ Γ2 A (UserExp). . . Figure 8: Core Language – Static Semantics (Vb) 26 A.4 Model PreType/Type Interpretation (Notation) χ ::= {(k, q, W, v), . . .} World Description (Notation) W ::= . . . ƒ CandAtomk = {(j, q, W, v) ∈ N × Quals × j