Gabriel Scherer

Max New

Nick Rioux

Amal Ahmed

FabULous Interoperability for ML and a Linear Language

Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.

Introduction

Feature accretion is a common trend among mature but actively evolving programming languages, including C++, Haskell, Java, OCaml, Python, and Scala. Each new feature strives for generality and expressiveness, and may provide a large usability improvement to users of the particular problem domain or programming style it was designed to empower (e.g., XML documents, asynchronous communication, staged evaluation). But feature creep in general-purpose languages may also make it harder for programmers to master the language as a whole, degrade the user experience (e.g., leading to more cryptic error messages), require additional work on the part of tooling providers, and lead to fragility in language implementations.

A natural response to increased language complexity is to define subsets of the language designed for a better programming experience. For instance, a subset can be easier to teach (e.g., "Core" ML4 , Haskell 98 as opposed to GHC Haskell, Scala mastery levels5 ); it can facilitate static analysis or decrease the risk of programming errors, while remaining sufficiently expressive for the target users' needs (e.g., MISRA C, Spark/Ada); it can enforce a common style within a company; or it can be designed to encourage a transition to deprecate some ill-behaved language features (e.g., strict Javascript).

Once a subset has been selected, it may be the case that users write whole programs purely in the subset (possibly using tooling to enforce that property), but programs will commonly rely on other libraries that are not themselves implemented in the same subset of the language. If users stay in the subset while using these libraries, they will only interact with the part of the library whose interface is expressible in the subset. But does the behavior of the library respect the expectations of users who only know the subset? When calling a function from within the subset breaks subset expectations, it is a sign of leaky abstraction.

How should we design languages with useful subsets that manage complexity and avoid abstraction leaks?

We propose to look at this question from a different, but equivalent, angle: instead of designing a single big monolithic language with some nicer subsets, we propose to consider multi-language programming systems where several smaller programming languages interact together to cover the same feature space. Each language or sub-combination of languages is a subset, in the above sense, of the multi-language, and there is a clear definition of abstraction leaks in terms of user experience: a user who only knows some of the languages of the system should be able to use the multi-language system, interacting with code written in the other languages, without have their expectations violated. If we write a program in Java and call a function that, internally, is implemented in Scala, there should be no surprises-our experience should be the same as when calling a pure Java function. Similarly, consider the subset of Haskell that does not contain IO (input-output as a type-tracked effect): the expectations of a user of this language, for instance in terms of valid equational reasoning, should not be violated by adding IO back to the language-in the absence of the abstraction-leaking unsafePerformIO.

We propose a formal specification for a "no abstraction leaks" guarantee that can be used as a design criterion to design new multi-language systems, with graceful interoperation properties. It is based on the formal notion of full abstraction which has previously been used to study the denotational semantics of programming languages [START_REF] Meyer | Towards fully abstract semantics for local variables[END_REF][START_REF] Milner | Fully abstract models of typed lambda calculi[END_REF][START_REF] Cartwright | Observable sequentiality and full abstraction[END_REF], Jeffrey and Rathke, 2005, Abramsky, Jagadeesan, and Malacaria, 2000], and the formal property of compilers [Ahmed andBlume, 2008, 2011, Devriese, Patrignani, and Piessens, 2016, New, Bowman, and Ahmed, 2016, Patrignani, Agten, Strackx, Jacobs, Clarke, and Piessens, 2015], but not for userfacing languages. A compiler C from a source language S to a target language T is fully abstract if, whenever two source terms s 1 and s 2 are indistinguishable in S, their translations C(s 1 ) and C(s 2 ) are indistinguishable in T . In a multi-language G+E formed of a general-purpose, user-friendly language G and a more advanced language E-one that provides an escape hatch for experts to write code that can't be implemented in G-we say that E does not leak into G if the embedding of G into the multi-language G + E is fully abstract.

To demonstrate that our formal specification is reasonable, we design a novel multi-language programming system that satisfies it. Our multi-language λ UL combines a general-purpose functional programming language λ U (unrestricted) of the ML family with an advanced language λ L (linear) with linear types and linear state. It is less convient to program in λ L 's restrictive type system, but users can write programs in λ L that could not be written in λ U : they can use linear types, locally, to enforce resource usage protocols (typestate), and they can use linear state and the linear ownership discipline to write programs that do in-place update to allocate less memory, yet remain observationally pure.

Consider for example the following mixed-language program. The blue fragments are written in the general-purpose, user-friendly functional language, while the red fragments are written in the linear language. The boundaries UL and LU allow switching between languages. The program reads all lines from a file, accumulating them in a list, and concatenating it into a single string when the end-of-file (EOF) is reached. The linear type system ensures that the file handle is properly closed: removing the close handle call would give a type error. On the other hand, only the parts concerned with the resource-handling logic need to be written in the red linear language; the user can keep all general-purpose logic (here, how to accumulate lines and what to do with them at the end) in the more convenient generalpurpose blue language-and call this function from a blue-language program. Fine-grained boundaries allow users to rely on each language's strength and to use the advanced features only when necessary.

In this example, the file-handle API specifies that the call to line, which reads a line, returns the data at type ![String]. The latter represents how U values of type String can be put into a lump type to be passed to the linear world where they are treated as opaque blackboxes that must be passed back to the ML world for consumption. For other examples, such as in-place list manipulation or transient operations on an persistent data structure, we will need a deeper form of interoperability where the linear world creates, dissects or manipulates U values. To enable this, our multi-language supports translation of types from one language to the other, using a type compatibility relation σ σ between λ U types σ and λ L types σ.

We claim the following contributions:

1. We propose a formal specification of what it means for advanced language features to be introduced in a (multi-)language system without introducing a class of abstraction leaks that break equational reasoning. This specification captures a useful usability property, and we hope it will help us and others design more usable programming languages, much like the formal notion of principal types served to better understand and design type inference systems. 2. We design a simple linear language, λ L , that supports linear state (Section 2).

This simple design for linear state is a contribution of its own. A nice property of the language (shared by some other linear languages) is that the code has both an imperative interpretation-with in-place memory update, which provides resource guarantees-and a functional interpretation-which aids program reasoning. The imperative and functional interpretations have different resource usage, but the same input/output behavior. 3. We present a multi-language programming system λ UL combining a core ML language, λ U (U for Unrestricted, as opposed to Linear) with λ L and prove that the embedding of the ML language λ U in λ UL is fully abstract (Section 3). Moreover, the multi-language is designed to ensure that our full abstraction result is stable under extension of the embedded ML language λ U . 4. We define a logical relation and prove parametricity for λ UL . The logical relation illustrates, semantically, why one can reason functionally about programs in λ UL despite the presence of state and strong updates (Section 4). 5. We evaluate the resulting language design by providing examples of hybrid λ UL programs that exhibit programming patterns inaccessible to ML alone, such that safe in-place updates and typestate-like static protocol enforcement (Section 5).

2 The λ U and λ L languages The novelty lies in the linear language λ L , which we present in several steps. As is common in λ-calculi with references, the small-step operational semantics is given for a language that is not exactly the surface language in which programs are written, because memory allocation returns locations that are not in the grammar of surface terms. Reductions are defined on configurations, a local store paired with a term in a slightly larger internal language. We have two type systems, a type system on surface terms, that does not mention locations and stores-which is the one a programmer needs to know-and a type system on configurations, which contains enough static information to reason about the dynamics of our language and prove subject reduction. Again, this follows the standard structure of syntactic soundness proofs for languages with a mutable store.

Types σ ::= α | σ1 × σ2 | 1 | σ1 → σ2 | σ1 + σ2 | µα. σ | ∀α. σ
Values v ::= x | v1, v2 | | λ(x : σ). e | inj 1 v | inj 2 v | foldµα.σ v | Λα. v Contexts Γ ::= • | Γ , x : σ | Γ , α
We present the surface language and type system in Section 2.1, except for the language fragment manipulating the linear store which is presented in Section 2.2. Finally, the internal terms, their typing and reduction semantics are presented in Section 2.3.

The Core of λ L

Figure 3 presents the surface syntax of our linear language λ L . For the syntactic categories of types σ, and expressions e, the last line contains the constructions related to the linear store that we only discuss in Section 2.2.

Types

σ ::= σ1 ⊗ σ2 | 1 | σ1 σ2 | σ1 ⊕ σ2 | µα. σ | α | !σ | Box 1 σ | Box 0
Expr. In technical terms, our linear type system is exactly propositional intuitionistic linear logic, extended with iso-recursive types. For simplicity and because we did not need them, our current system also does not have polymorphism or additive/lazy pairs σ 1 & σ 2 . Additive pairs would be a trivial addition, but polymorphism would require more work when we define the multi-language semantics in Section 3.

In less technical terms, our type system can enforce that values be used linearly, meaning that they cannot be duplicated or erased, they have to be deconstructed exactly once. Only some types have this linearity restriction; others allow duplication and sharing of values at will. We can think of linear values as resources to be spent wisely; for any linear value somewhere in a term, there can be only one way to access this value, so we can interpret the language as enforcing an ownership discipline where whoever points to a linear value owns it.

The types of linear values are the type of linear pairs σ 1 ⊗ σ 2 , of linear disjoint unions σ 1 ⊕ σ 2 , of linear functions σ 1 σ 2 , and of the linear unit type 1. For example, a linear function must be called exactly once, and its result must in turn be consumed -such linear functions can safely capture linear resources. The expression-formers at these types use the same syntax as the unrestricted language λ U , with the exception of linear pair deconstruction let v 1 , v 2 = e 1 in e 2 , which names both members of the deconstructed pair at once. A linear pair type with projection would only ever allow to observe one of the two members; this would correspond to the additive/lazy pairs σ 1 & σ 2 , where only one of the two members is ever computed.

The types of non-linear, duplicable values are the types of the form !σ-the exponential modality of linear logic. If e has type σ, the term share e has type !σ. Values of this type are not uniquely owned, they can be shared at will. If the term e has duplicable type !σ, then the term copy e has type σ: this creates a local copy of the value that is uniquely-owned by its receiver and must be consumed linearily.

This resource-usage discipline is enforced by the surface typing rules of λ L , presented in Figure 4. They are exactly the standard (two-sided) logical rules of intuitionistic linear logic, annotated with program terms. The non-duplicability of linear values is enforced by the way contexts are merged by the inference rules: if e 1 is type-checked in the context Γ 1 and e 2 in Γ 2 , then the linear pair e 1 , e 2 is only valid in the combined context Γ 1 Γ 2 . The ( ) operation is partial; this combined context is defined only if the variables shared by Γ 1 and Γ 2 are duplicable-their type is of the form !σ. In other words, a variable at a non-duplicable type in Γ 1 Γ 2 cannot possibly appear in both Γ 1 and Γ 2 : it must appear exactly once6 .

Γ 1 Γ 2 (Γ 1, x : !σ) (Γ 2, x : !σ) def = (Γ 1 Γ 2), x : !σ (Γ 1, x : σ) Γ 2 def = (Γ 1 Γ 2), x : σ (x / ∈ Γ 2) Γ Γ l case e of x1. e1 | x2. e2 : σ !Γ l e : σ !Γ l share e : !σ Γ l e : !σ Γ l copy e : σ µα. σ unfold - ›- foldµα.σ σ[µα. σ/α] 1 new - ›- free Box 0 Box 1 σ unbox - ›- box (Box 0 ) ⊗ σ
A good way to think of the linear judgment Γ l e : σ is that the evaluation of e consumes the linear variables of Γ ; it is thus natural that the strict pair e 1 , e 2 would need separate sets of resources Γ 1 and Γ 2 , as it evaluates both members to return a value. On the other hand, case elimination case e of x 1 . e 1 | x 2 . e 2 reuses the same context Γ in both branches e 1 and e 2 : only one will be evaluated, so they do not compete for resources.

The variable rule does not expect a context of the form Γ , x : σ but of the form !Γ , x : σ. Here !Γ is a notation for the pointwise application of the (!) connective to all the types in Γ -i.e., all types in !Γ are of the form !σ. This means that the variable rule can only be used when all variables in the context are duplicable, except maybe the variable that is being used. A context of the form Γ , x : σ would allow us to forget some variable present in the context; in our judgment Γ l e : σ, all non-duplicable variables in Γ must appear (once) in e.

The form !Γ is also used in the typing rule for share e: a term can only be made duplicable if it does not depend on linear resources from the context. Otherwise, duplicating the shared value could break the unique-ownership discipline on these linear resources.

Finally, the linear isomorphism notation for fold and unfold in Figure 4 defines them as primitive functions, at the given linear function type, in the empty context -using them does not consume resources. This notation also means that, operationally, these two operations shall be inverses of each other. The rules for the linear store type Box 1 σ and Box 0 are described in Section 2.2.

Lemma 1 (Context joining properties) Context joining ( ) is partial but associative and commutative. In particular, if (Γ 1 Γ 2 ) Γ is defined, then both Γ i Γ are defined.

Linear Memory in λ L

The surface typing rules for the linear store are given at the end of Figure 4. The linear type Box 1 σ represents a memory location that holds a value of type σ. The type Box 0 represents a location that has been allocated, but does not currently hold a value. The primitive operations to act on this type are given as linear isomorphisms: new allocates, turning a unit value into an empty location; conversely, free reclaims an empty location. Putting a value into the location and taking it out are expressed by box and unbox , which convert between a pair of an empty location and a value, of type (Box 0 ) ⊗ σ, and a full location, of type Box 1 σ.

For example, the following program takes a full reference and a value, and swaps the value with the content of the reference:

λ(p : (Box 1 σ) ⊗ σ). let r, x = p in let l, x l = unbox r in box l, x , x l
The programming style following from this presentation of linear memory is functional, or applicative, rather than imperative. Rather than insisting on the mutability of references-which is allowed by the linear discipline-we may think of the type Box 1 σ as representing the indirection through the heap that is implicit in functional programs. In a sense, we are not writing imperative programs with a mutable store, but rather making explicit the allocations and dereferences happening in higher-level purely functional language. In this view, empty cells allow memory reuse.

This view that Box 1 σ represents indirection through the memory suggests we can encode lists of values of type σ by the type LinList σ

def = µα. 1 ⊕ Box 1 (σ ⊗ α).
The placement of the box inside the sum mirrors the fact that empty list is represented as an immediate value in functional languages. From this type definition, one can write an in-place reverse function on lists of σ as follows:

fix λ(rev_into : LinList σ LinList σ LinList σ). λ(xs : LinList σ). λ(acc : LinList σ). case unfold xs of | y. (y; acc) | y. let l, p = unbox y in let xs, x = p in rev_into xs (fold (inj2 (box l, x, acc )))
This definition uses a fixpoint operator fix that can be defined, in the standard way, using the iso-recursive type µα. α σ σ of the strict fixpoint combinator on functions σ σ .

Our linear language λ L is a formal language that is not terribly convenient to program directly. We will not present a full surface language in this work, but one could easily define syntactic sugar to write the exact same function as follows:

rev_into Nil acc = acc rev_into (Cons x, xs @ l) acc = rev_into xs (Cons x, acc @ l)

One can read this function as the usual functional rev_append function on lists, annotated with memory reuse information: if we assume we are the unique owner of the input list and won't need it anymore, we can reuse the memory of its cons cells (given in this example the name l) to store the reversed list. On the other hand, if you read the box and unbox as imperative operations, this code expresses the usual imperative pointer-reversal algorithm.

This double view of linear state occurs in other programming systems with linear state. It was recently emphasized in O'Connor, Chen, Rizkallah, Amani, Lim, Murray, Nagashima, Sewell, and Klein [2016], where the functional point of view is seen as easing formal verification, while the imperative view is used as a compilation technique to produce efficient C code from linear programs.

Internal λ L Syntax and Typing

To give a dynamic semantics for λ L and prove it sound, we need to extend the language with explicit stores and store locations. Indeed, the allocating term new should reduce to a "fresh location" allocated in some store s, and neither are part of the surface-language syntax. The corresponding internal typing judgment is more complex, but note that users do not need to know about it to reason about correctness of surface programs. The internal typing is essential for the soundness proof, but also useful for defining the multi-language semantics in Section 3.

The syntax of internal terms and the internal type system are presented in Figure 5. Reduction will be defined on configurations (s | e), which are pairs of a store s and a term e. Stores s map locations to either nothing (the location is empty), written [ → •], or a value paired with its own local store, noted

[ → (s | v)].
Having local stores in this way, instead of a single global store as is typical in formalizations of ML, directly expresses the idea of "memory ownership" in the syntax: a term e "owns" the locations that appear in it, and a configuration (s | e) is only well-typed if the domain of s is exactly those locations. Each store slot, in turn, may contain a value and the local store owned by the value; in particular, passing a full location of type Box 1 σ transfers ownership of the location, but also of the store fragment captured by the value.

Our internal typing judgment Ψ ; Γ l s | e : σ checks configurations, not just terms, and relies not only on a typing context for variables Γ but also on a store typing Ψ , which maps the locations of the configuration to typing assumptions of two forms: (•; • : Box 0 ) indicates that must be empty in the configuration, and (Γ ; Ψ : Box 1 σ) indicates that is full, and that the value it contains owns a local store of type s and the resources in Γ .

Just as linear variables must occur exactly once in a term, locations have linear types and thus occur exactly once in a term. Our typing judgment uses disjoint store typings Ψ 1 Ψ 2 to enforce this linearity. Similarly, leaf rules such as the variable, unit, and location rules enforce that both the store typing and the store be empty, which enforces that all locations are used in the term.

Locations are always linear, never duplicable. To allow sharing terms that contain locations, the internal language uses the internal construction share(s : Ψ ). e, that captures a local store s : Ψ . This notation is a binding construct: the locations in s are bound by this shared term, and not visible outside this term. In particular, the typing rule for share(s : Ψ ). e checks the term e in the store s, but it is itself only valid paired with an empty store, under the empty store typing. When new copies of a shared term are made, the local store is copied as well: this is necessary to guarantee that locations remain linear-and for correctness of linear state update.

The typing rule for functions λ(x : σ). e lets function bodies use an arbitrary store typing Ψ . This would be unsound if our functions were duplicable, but it is a natural and expressive choice for linear, one-shot functions. To make a function duplicable, one can share it at type !(σ σ ), whose values are of the canonical

= • • • | | share(s : Ψ ). v Store s ::= ∅ | s[ → (s | v)] | s[ → •] Configurations ::= (s | e)
Store typing

Ψ ::= • | Ψ , (•; • : Box 0 ) | Ψ , (Ψ ; Γ : Box 1 σ) s1 + + s2
Union of stores on disjoint locations Ψ 1 Ψ 2 Union of store typings on disjoint locations ). e, any term e of the surface language (Figure 3) can be seen as a term of the internal language (Figure 5). In particular, we can prove that the surface and internal typing judgments coincide on surface terms.

Ψ ; Γ l s | e : σ Γ l e : σ def = •; Γ l ∅ | e : σ Ψ 1; Γ 1 l s1 | e1 : σ1 Ψ 2; Γ 2 l s2 | e2 : σ2 Ψ 1 Ψ 2; Γ 1 Γ 2 l s1 + + s2 | e1, e2 : σ1 ⊗ σ2 Ψ ; Γ l s | e : σ1 ⊗ σ2 Ψ ; Γ , x1 : σ1, x2 : σ2 l s | e : σ Ψ Ψ ; Γ Γ l s + + s | let x1, x2 = e in e : σ •; !Γ , x : σ l ∅ | x : σ •; !Γ l ∅ | : 1 Ψ ; Γ l s | e : 1 Ψ ; Γ l s | e : σ Ψ Ψ ; Γ Γ l s + +
Ψ ; Γ l s | e : σ1 ⊕ σ2 Ψ ; Γ , x1 : σ1 l s | e1 : σ Ψ ; Γ , x2 : σ2 l s | e2 : σ Ψ Ψ ; Γ Γ l s + + s | case e of x1. e1 | x2. e2 : σ Ψ ; !Γ l s | e : σ •; !Γ l ∅ | share(s : Ψ ). e : !σ Ψ ; Γ l s | e : !σ Ψ ; Γ l s | copy e : σ (•; • : Box 0 ); !Γ l [ → •] | : Box 0 Ψ ; Γ l s | v : σ (Ψ ; Γ : Box 1 σ); Γ !Γ l [ → (s | v)] | : Box 1 σ µα. σ unfold - ›- foldµα.σ σ[µα. σ/α] 1 new - ›- free Box 0 Box 1 σ unbox - ›- box (Box 0 ) ⊗ σ
Lemma 2 If e is a surface term of λ L , then the surface judgment Γ l e : σ holds if and only if the internal judgment •; Γ l ∅ | e : σ holds.

The following technical results are used in the soundness proof for the language -the subject-reduction result.

Lemma 3 (Inversion principle for λ L values) In any complete derivation of Ψ ; Γ l s | v : σ, either v is a variable x, or the derivation starts with the introduction rule for σ.

For example, if we have Ψ ; Γ l s | v : !σ, then we know that v is either a variable or of the form share(s : Ψ ). v for some v , but also that s = ∅, Ψ = • and that Γ is of the form !Γ for some Γ . The latter is immediate if v is share(s : Ψ ). v , and also holds if v is a variable.

Lemma 4 (Weakening by duplicable contexts)

Ψ ; Γ l s | e : σ implies Ψ ; !Γ , Γ l s | e : σ.

Reduction of Internal Terms

Figure 6 gives a small-step operational semantics for the internal terms of λ L .

We separate the head reductions ( L ) from reductions in depth ( L →). The head reduction of the linear types of the core language do not involve the store and are standard. For the store primitives of Figure 4 acting on Box 0 , Box 1 σ, we reuse the isomorphism notation to emphasize that the related primitives are inverses of each other.

There are several reduction rules for copy (share e), one for each type connective. These reductions perform a deep copy of the value, stopping only on ground data ( ), function values, and shared sub-terms: when copying a !!σ into a !σ, there is no need for a deep copy. When it encounters a location, copy (share ) reduces to a new allocation. If the location contains a value, the new location is filled with a copy of this value.

The copying rule for functions performs a copy of the local store s of the shared function. The locations in s are bound on the left-hand-side of the reduction, and free on the right-hand-side: this reduction step allocates fresh locations, and the store typing of the term changes from • on the left to Ψ on the right. The fact that reduction changes the store typing is not unique to this rule, it is also the case when directly copying locations. In ML languages with references, the store only grows during reduction. That is not the case for our linear store: our reduction may either allocate new locations or free existing ones. case

(inj i v) of x1. e1 | x2. e2 L ei[v/xi] unfold (foldµα.σ v) L v e L e (s | e) L (s | e ) (∅ | ) new L L free ([ → •] | ) (s[ → •] | , v ) box L L unbox ([ → (s | v)] | ) copy (share(s1 + + s2 : Ψ 1 Ψ 2). v1, v2 ) L if locs(si) = locs(Ψ i) = locs(vi) copy share(s1 : Ψ 1). v1, copy share(s2 : Ψ 2). v2 copy (share(∅ : •). ) L copy (share(s : Ψ ). inj i v) L inj i copy (share(s : Ψ ). v) copy (share(s : Ψ ). fold v) L fold (copy (share(s : Ψ ). v)) (∅ | copy (share(s : Ψ ). λ(x : σ). e)) L (s | λ(x : σ). e) copy (share(∅ : •). (share(s : Ψ ). v)) L share(s : Ψ ). v copy (share([ → •] : (•; • : Box 0 )). ) L new copy (share([ → (s | v)] : (Ψ ; !Γ : Box 1 σ)). ) L box new , copy (share(s : Ψ ). v) linear reduction contexts Ψ ; Γ l s | K[ : σ] : σ K ::= : σ | K, e2 | v, K | let v1, v2 = K in e2 | K; e | K e | v K | copy K | inj1 K | inj2 K | case K of x1. e1 | x2. e2 | foldµα.σ K | unfold K | new K | free K | box K | unbox K typing rules of terms, plus: •; • l ∅ | ( : σ) : σ reduction (s | e) L → (s | e ) (s | e) L (s | e ) (s | e) L → (s | e ) Ψ ; Γ l s | K[ : σ] : σ (s | e) L → (s | e ) (s + + s | K[e]) L → (s + + s | K[e ]) Ψ ; Γ l s | e : σ (s | e) L → (s | e ) Ψ ; Γ l s | e : σ (∅ | share(s : Ψ ). e) L → (∅ | share(s : Ψ ). e )
Fig. 6. Linear Language: Operational Semantics

We define a grammar of (deterministic) reduction contexts, which contain exactly one hole in evaluation position. However, we only define linear contexts K that do not share their hole: we need a specific treatment of the share(s : Ψ ). e reduction. Its subterm e is reduced in the local store s, but may create or free locations in the store; so we need to update the local store and its store typing during the reduction. Proof. By induction on the typing derivation of e, using induction hypothesis in the evaluation order corresponding to the structure of contexts K. If one induction hypothesis returns a reduction, we build a bigger reduction ( L →) for the whole term. If all induction hypotheses return a value, the proof depends on whether the head term-former is an introduction/construction form or an elimination/destruction form. An introduction form whose subterms are values is a value. For elimination forms, we use Lemma 3 (Inversion principle for λ L values) on the eliminated subterm (a value), to learn that it starts with an introduction form, and thus forms a head redex with the head elimination form, so we build a head reduction ( L ).

Lemma 5 (Non-store-escaping substitution principle)

If Ψ ; Γ , x : σ l s | e : σ Ψ ; Γ l s | v : σ Γ Γ x / ∈ Ψ then Ψ Ψ ; Γ Γ l s + + s | e[v/x] : σ
Proof. The proof, summarized below, proceeds by induction on the typing derivation of e.

Most cases need an additional case analysis on whether the substituted type σ is a duplicable type of the form !σ , as it influence whether it may appear in zero or several subterms of e. (This is a price to pay for contraction and weakening happening in all rules for convenience, instead of being isolated in separate structural rules.)

For example, in the variable case, e may be the variable x itself, in which case we know that Γ is empty and conclude immediately. But e may also be another variable y if x is duplicable and has been dropped. In that case, we perform an inversion (Lemma 3) on the v premise to learn that Ψ is empty and Γ is duplicable, and can thus use Lemma 4 (Weakening by duplicable contexts).

In the e 1 , e 2 case, if x is a linear variable it only occurs in one subterm on which we apply our induction hypothesis. If x is duplicable, inversion on the v premises again tells us that Γ is duplicable. We know by assumption that (Γ 1 Γ 2 ) Γ ; because Γ is duplicable, we can deduce from Lemma 1 (Context joining properties) that the Γ i Γ are also defined, which let us apply an induction hypothesis on both subterms e i . To conclude, we need the computation

(Γ 1 Γ ) (Γ 2 Γ ) = Γ 1 Γ 2 (Γ Γ ) = Γ 1 Γ 2 Γ
which again comes from duplicability of Γ .

The assumption x / ∈ Ψ enforces that the resource x is consumed in the term e itself, not in one of the values [ → (s | v)] in the store: otherwise x would appear in the store typing (Γ ;

Ψ : Box 1 ) of this location in Ψ . It is used in the case where e : σ is a full location : Box 1 σ . If x could appear in the value of in the store, we would have substitute it in the store as well -in our substitution statement, only the term is modified. Here we know that this value is unused, so it has a duplicable type and we can perform an inversion in the other cases. Proof. The proof is done by induction on the reduction derivation.

The head-reduction rules involving substitutions rely on Lemma 5 (Nonstore-escaping substitution principle); note that in each of them, for example (λ(x : σ ). e ) e , the substituted variable x is bound in the term e, and thus does not appear in the store s: the non-store-escaping hypothesis holds.

For the copy rule and the store operators, we build a valid derivation for the reduced configuration by inverting the typing derivation of the reducible configuration.

In the non-head-reduction cases, the share case is by direction, and the context case K[e] uses Lemma 6 (Context decomposition) to obtain a typing derivation for e, and the same lemma again rebuild a derivation of the reduced term K[e ].

Multi-language semantics

To formally define our multi-language semantics we create a combined language λ UL which lets us compose term fragments from both λ U and λ L together, and we give an operational semantics to this combined language. Interoperability is enabled by specifying how to transport values across the language boundaries.

Multi-language systems in the wild are not defined in this way: both languages are given a semantics, by interpretation or compilation, in terms of a shared lower-level language (C, assembly, the JVM or CLR bytecode, or Racket's core forms), and the two languages are combined at that level. Our formal multilanguage description can be seen as a model of such combinations, that gives a specification of the expected observable behavior of this language combination. Another difference from multi-languages in the wild is our use of very finegrained language boundaries: a term written in one language can have its subterms written in the other, provided the type-checking rules allow it. Most multilanguage systems, typically using Foreign Function Interfaces, offer coarsergrained composition at the level of compilation units. Fine-grained composition of existing languages, as done in the Eco project [START_REF] Barrett | Finegrained language composition: A case study[END_REF], is difficult because of semantic mismatches. In Section 5 (Hybrid program examples) we demonstrate that fine-grained composition is a rewarding language design, enabling new programming patterns.

Lump Type and Language Boundaries

The core components the multi-language semantics are shown Figure 7-the communication of values from one language to the other will be described in the next section. The multi-language λ UL has two distinct syntactic categories of types, values, and expressions: those that come from λ U and those that come from λ L . Contexts, on the other hand, are mixed, and can have variables of both sorts. For a mixed context Γ , the notation !Γ only applies (!) to its linear variables.

The typing rules of λ U and λ L are imported into our multi-language system, working on those two separate categories of program. They need to be extended to handle mixed contexts Γ instead of their original contexts Γ and Γ . In the linear case, the rules look exactly the same. In the ML case, the typing rules implicitly duplicate all the variables in the context. It would be unsound to extend them to arbitrary linear variables, so they use a duplicable context !Γ .

To build interesting multi-language programs, we need a way to insert a fragment coming from a language into a term written in another. This is done using language boundaries, two new term formers LU(e) and UL(s : Ψ | e) that inject an ML term into the syntactic category of linear terms, and a linear configuration into the syntactic category of ML terms.

Of course, we need new typing rules for these term-level constructions, clarifying when it is valid to send a value from λ U into λ L and vice versa. It would be incorrect to allow sending any type from one language into the other-for instance, by adding the counterpart of our language boundaries in the syntax of types-since values of linear types must be uniquely owned so they cannot possibly be sent to the ML side as the ML type system cannot enforce unique ownership.

On the other hand, any ML value could safely be sent to the linear world. For closed types, we could provide a corresponding linear type (1 maps to !1, etc.), but an ML value may also be typed by an abstract type variable α, in which case we can't know what the linear counterpart should be. Instead of trying to provide translations, we will send any ML type σ to the lump type [σ], which embeds ML types into linear types. A lump is a blackbox, not a type translation: the linear language does not assume anything about the behavior of its values-the values of [σ] are of the form [v], where v : σ is an ML value that the linear world cannot use. More precisely, we only propagate the information that ML values are all duplicable by sending σ to ![σ].

Types σ | σ σ (unchanged from Figure 1) The typing rules for language boundaries insert lumps when going from λ U to λ L , and remove them when going back from λ L to λ U . In particular, arbitrary linear types cannot occur at the boundary, they must be of the form ![σ].

σ + ::= • • • | [σ] Values v | v v (unchanged from Figure 1) v + ::= • • • | [v]
LU(v) L [v] UL(∅ : • | share [v]) U → v Ψ | Γ ul s | e : σ (s | e) L → (s | e ) Ψ | Γ ul s | e : σ UL(s : Ψ | e) U → UL(s : Ψ | e )
Finally, boundaries have reduction rules: a term or configuration inside a boundary in reduction position is reduced until it becomes a value, and then a lump is added or removed depending on the boundary direction. Note that because the v in UL(s : Ψ | v) is at a duplicable type ![σ], we know by inversion that the store is empty.

Interoperability: Static Semantics

If the linear language could not interact with lumped values at all, our multilanguage programs would be rather boring, as the only way for the linear extension to provide a value back to ML would be to have received it from λ U and pass it back unchanged (as in the lump embedding of [START_REF] Matthews | Operational semantics for multilanguage programs[END_REF]). To provide a real interaction, we provide a way to extract values out of a lump ![σ], use it at some linear type σ, and put it back in before sending the result to λ U .

Interoperability context Σ ::= • | Σ, α !β Compatibility relation Σ ul σ σ with σ σ def = • ul σ σ Σ ul 1 !1 Σ ul σ1 !σ1 Σ ul σ2 !σ2 Σ ul σ1 × σ2 !(σ1 ⊗ σ2) Σ ul σ1 !σ1 Σ ul σ2 !σ2 Σ ul σ1 + σ2 !(σ1 ⊕ σ2) Σ ul σ !σ Σ ul σ !σ Σ ul σ → σ !(!σ !σ ) Σ ul σ ![σ] Σ ul σ !σ Σ ul σ !!σ Σ ul σ !σ Σ ul σ !(Box 1 σ) Σ, α !β ul σ !σ Σ ul µα. σ !(µβ. σ) (α !β) ∈ Σ Σ ul α !β
Interoperability primitives and derived constructs: The correspondence between intuitionistic types σ and linear types σ is specified by a heterogeneous compatibility relation σ σ defined in Figure 8 (Multi-language: Static Interoperability Semantics). The specification of this relation is that if σ σ holds, then the space of values of ![σ] and σ are isomorphic: we can convert back and forth between them. When this relation holds, the term-formers lump σ and σ unlump perform the conversion. (The position of the index σ emphasizes that the input e of lump σ e has type σ, while the output of σ unlump e has type σ.)

![σ] σ unlump - ›- lump σ σ whenever • ul σ σ σ LU(e)
For example, we have

![(σ→σ )] !(![σ] ![σ ]
). Given a lumped ML function, we can unlump it to see it as a linear function. We can call it from the linear side, but have to pass it a duplicable argument since an ML function may duplicate its argument. Conversely, we can convert a linear function into a lumped function type to pass it to the ML side, but it has to have a duplicable return type since the ML side may freely share the return value.

Our lump σ and σ unlump primitives are only indexed by the linear type σ, because a compatible ML type σ can be uniquely recovered, as per the following result.

Lemma 7 (Determinism of the compatibility relation) If σ σ and σ σ then σ = σ .

Proof. By induction on the syntax of σ: the judgment Σ ul σ σ is syntaxdirected in its σ component.

Note that the converse property does not hold: for a given σ, there are many σ such that σ σ. For example, we have 1 !1 but also 1 !!1. This corresponds to the fact that the linear types are more fine-grained, and make distinctions (inner duplicability, dereference of full locations) that are erased in the ML world. The σ ![σ] case also allows you to (un)lump as deeply or as shallowly as you need:

σ 1 × (σ 2 × σ 3 ) is compatible with both !(![σ 1 ] ⊗ ![σ 2 × σ 3 ]) and !(![σ 1 ] ⊗ (![σ 2 ] ⊗ ![σ 3 ])).
We could not systematically translate the complete type σ, as type variables cannot be translated and need to remain lumped. Allowing lumps to "stop" the translation at arbitrary depth is a natural generalization.

Lemma 8 (Substitution of recursive hypotheses) If Σ, α !β ul σ σ, α / ∈ σ, and

Σ ul σ !σ then Σ ul σ[σ /α] σ[σ /β].
Proof. By induction on the σ σ derivation. There are two leaf cases: the case recursive hypotheses, which is immediate, and the case of lump σ ![σ]. In this latter case, notice that σ is a type of λ U , so in particular it does not contain the variable β; and we assumed α / ∈ σ so we also have

α / ∈ σ, so σ[σ /α] = σ ![σ] = σ[σ /β].
The term LU(e) turns a e : σ into a lumped type ![σ], and we need to unlump it with some σ unlump for a compatible σ σ to interact with it on the linear side. It is common to combine both operations and we provide syntactic sugar for it: σ LU(e). Similarly UL σ (e) first lumps a linear term then sends the result to the ML world.

Interoperability: Dynamic Semantics

↔ !1 share v1 ↔ !σ 1 share(s1 : Ψ 1). v1 v2 ↔ !σ 2 share(s2 : Ψ 2). v2 locs(s1) = locs(Ψ 1) = locs(v1) locs(s2) = locs(Ψ 2) = locs(v2) v1, v2 ↔ !(σ 1 ⊗ σ 2 ) share(s1 + + s2 : Ψ 1 Ψ 2). v1, v2 v ↔ !σ i share(s : Ψ ). v inj i v ↔ !(σ 1 ⊕ σ 2 ) share(s : Ψ ). inj i v σ σ σ σ e → !(!σ !σ ) share λ(x : !σ). σ LU(e UL σ (x)) σ σ σ σ λ(x : σ). UL σ (copy e σ LU(x))) ← !(σ σ ) e v ↔ ![σ] share [v] v ↔ !σ share v v ↔ !!σ share (share v) v ↔ !σ share(s : Ψ ). v v ↔ !Box 1 σ share([ → (s | v)] : (•; Ψ : Box 1 σ)). v ↔ !σ[µα.σ/α] share(s : Ψ ). v foldµα.σ v ↔ !µα.σ share(s : Ψ ). (foldµα.σ v) (∅ | share [v]) σ unlump L L lump σ (∅ | v) whenever v → σ v whenever v ← σ v
Fig. 9. Multi-language: Dynamic Interoperability Semantics

We were careful to define the compatibility relation such that σ σ only holds when ![σ] and σ are isomorphic, in the sense that any value of one can be converted into a value of another. Figure 9 defines the operational semantics of the lumping and unlumping operations precisely as realizing these isomorphisms. For concision, we specify the isomorphisms as relations, following the inductive structure of the compatibility judgment itself. We write (↔) when a rule can be read bidirectionally to convert in either directions (assuming the same direction holds of the premises), and (←) or (→) for rules that only describe how to convert values in one direction. Proof. By induction on σ σ. In the variable leaf case, we know α / ∈ Σ. In the lump leaf case σ !

[σ], the goal σ[σ /α] ![σ[σ /α]] is immediate.
Theorem 3 (Value translations are functional) If σ σ, then for any closed value v : σ there is a unique v : σ such that v → σ v, and conversely for any closed value v : σ there is a unique v : σ such that v ← σ v.

Proof. Remark that in the statement of the term, when we quantify over all closed values v : σ, we implicitly assume that in the general case values of v live in the empty global store -otherwise we would have a value of the form Ψ ; • l s | v : σ. This is valid because all types σ in the image of the type-compatibility relation are duplicable types of the form !σ , so by Lemma 3 (Inversion principle for λ L values) we know that v is in fact of the form share(s : Ψ ). e , living in the empty store.)

The two sides of the result are proved simultaneously by induction on σ σ, using inversion to reason on the shapes of v and v. Note that the inductive cases remain on closed values: the only variable-binder constructions, λ-abstractions, do not use the recursion hypothesis.

In the recursive case µα. σ !(µα. σ), to use the induction hypothesis on the folded values we need to know that the unfolded types σ[µα. σ/α] and σ[µα. σ/α] are compatible. This is exactly Lemma 8 (Substitution of recursive hypotheses), using the hypothesis µα. σ !(µα. σ) itself.

Lemma 10 (Lumping cancellation) The lump conversions lump σ and σ unlump cancel each other modulo βη. In particular,

σ LU(UL σ (v)) = βη v UL σ ( σ LU(v)) = βη v
Proof. By induction on σ, and then by parallel induction on the derivations of type compatibility and value compatibility. The parallel cases are symmetric by definition, only the function case !(!σ !σ ) needs to be checked. A simple computation, using the induction hypothesis on the smaller types !σ and !σ , shows that composing the two function translations gives an η-expansion -plus the βη-steps from the induction hypotheses. Note that the β-η rules used (for functions and !_) have been proved admissible for the logical relation, so in particular sound with respect with contextual equivalence.

Implementation consideration In a realistic implementation of this multi-language system, we would expect the representation choices made for λ U and λ L to be such that, for some but not all compatible pairs σ σ, the types σ and σ actually have the exact same representation, making the conversion an efficient no-op. An implementation could even restrict the compatibility relation to accept only the pairs that can be implemented in this way. That is, it would reject some λ UL programs, but the "graceful interoperability" result that is our essential contribution would still hold.

Full Abstraction from λ U into λ UL

We can now state and prove the major meta-theoretical result of this work, which is the proposed multi-language design extends the simple language λ U in a way that provably has, in a certain sense, "no abstraction leaks".

Multi-language parametricity

We discussed the design choice of manipulating lumps [σ] of any ML type, not just the type variable that motivates them. In the presence of polymorphism, this generalization is also an important design choice to preserve parametricity.

Let us define id σ (e) def = lump σ ( σ unlump e), and consider a polymorphic term of the form Λα. UL(. . . id ![α] . . . ). The (un)lumping operations on a lumped type such as ![α] are just the identity: the lumped value is passed around unchanged, so id ![α] (v) will reduce to v. Now, if we instantiate this polymorphic term with a ML type σ, it will reduce to a term UL(. . . id ![σ] . . . ) whose unlumping operation is still on a lumped type, so is still exactly the identity.

On the contrary, if we allowed lumps only on type variables, we would have to push the lump inside σ, and the (un)lumping operations would become more complex: if σ starts with an ML product type _ × _, it would be turned into a shared linear pair !(_ ⊗ _) by unlumping, and back into an ML pair by lumping. In general, id σ may perform deep η-expansions of lumped values. The fact that, after instantiation of the polymorphic term, we get a monomorphic term that has different (but η-equivalent) computational behavior would cause meta-theoretic difficulties; this is the approach that was adopted in previous work on multilanguages with polymorphism by Perconti and Ahmed [2014], and it made some of their proofs using a logical relations argument substantially more complicated. In the logical relation, polymorphism is obtained by allowing each polymorphic variable to be replaced by two types related by an "admissible" relation R, and the notion of admissibility of this previous work had to force relations to be compatible with η-expansion, which complicates the proofs.

In contrast, our handling of lump types as turning arbitrary types into blackboxes makes type instantiation obviously parametric. To formally demonstrate this aspect of our design, we develop a step-indexed logical relation (Figure 10) that proves that our multi-language satisfies a strong parametricity property that is not disrupted by the linear sublanguage or the cross-language boundaries.

The logical relation is a family of relations indexed by closed "relational types" which extend the grammar of σ, σ, which include a case for admissible relations R that is used to enable parametric arguments. The step index j in the definitions decreases strictly whenever related values of a type σ or σ are defined in terms of a non-strictly-smaller type; this happens in the definition of the relation at recursive types V µα. σ j . Because the language is non-terminating, our relation does not define an equivalence but an approximation: two expressions (e 1 , e 1 ) are related in E σ j if e 1 approximates e 2 : if e 1 reduces to a value in less than j steps, then e 2 must reduce to a related value.

The definition of admissible relations Rel[σ 1 , σ 2 ], used to define when λ U values of polymorphic types are related, V ∀α. σ , is completely standard, which demonstrates that our notion of boundaries preserves simple parametricity reasoning.

Although we have a stateful linear language, the logical relations for the linear types have more in common with a language with explicit closures-this is another consequence of the remark in Section 2.2 (Linear Memory in λ L ) that the language can also be interpreted using a functional semantics. The relations for closed λ L values and expressions, V σ and E σ , are indexed by a type but do not depend on a store typing: the related values may have different, non-empty store typings. This allows to relate two programs that are equivalent but allocate different references in different ways. Furthermore, since all state is linear, we don't need additional machinery to relate stores, since all the values in a store owned by a value will be reflected in the value. For example, the relation for empty locations V Box 0 relates any two arbitrary (empty) locations, and the relation for non-empty locations V Box 1 σ relates possibly-distinct locations that contain related values.

Logical relations effectively translate global invariants of the system into properties of type connectives. For example, consider the reduction rule for lumped values: UL(∅ :

• | share [v]) U → v.
In this rule we implicitly assumed that a linear value of the shape [v] at type ![σ] would occur in an empty local store. The term share [v] desugars into share(∅ : •). [v], but it is not immediately obvious that this should always be the case since it is possible to compute a value of type ![σ] by allocating references and using them. The intuitive reason why the store becomes empty when a value [v] is reached is that linear sub-terms e within v may only occur within a language boundary UL(s : Ψ | e): linear sub-terms have their own local store, so there are no globally visible linear locations for [v] to refer to. This global reasoning is elegantly expressed in a type-directed way in our logical relation by the definition of related values at lump type, which encodes the invariant that they always have an empty store:

V [σ] j def = {((∅ | [v 1 ]), (∅ | [v 2 ])) | (v 1 , v 2 ) ∈ V σ j }
From the logical relation defined on closed λ UL terms and values, we define logical approximation relations on open terms Γ e 1 log e 2 : σ and Γ l (s 1 | e 1 ) log (s 2 | e 2 ) : σ by asking for the open terms and values to be related under all related environments in the standard way-see Appendix A for full details. This lets us demonstrate the Fundamental Property to validate the construction of our logical relation, showing that all typing rules are admissible.

Theorem 4 (Fundamental Property) We also prove that the logical relation is sound with respect to contextual equivalence. For this, we define contextual approximation relations Γ e 1 ctx e 2 : σ and Γ l (s 1 | e 1 ) ctx (s 2 | e 2 ) : σ, by asking that e 1 , (s 1 | e 1 ) terminate more often than e 2 , (s 2 | e 2 ) when run under arbitrary contexts-see Appendix A for details.

1. If !Γ u e : σ then !Γ e log e : σ Atom[σ] def = {v | • u v : σ} Rel[σ1, σ2] def = {R : N → P(Atom[σ1] × Atom[σ2]) | ∀j ≤ j . R j ⊂ R j } V R j def = R j V σ1 → σ2 j def = {(λ(x1 : (σ1)1). e1, λ(x2 : (σ1)2). e2) | ∀j ≤ j, (v1, v2) ∈ V σ1 j . (e1[v1/x1], e2[v2/x2]) ∈ E σ2 j } V ∀α. σ j def = {(Λα. v1, Λα. v2) | ∀σ1, σ2, R ∈ Rel[σ1, σ2]. (v1, v2) ∈ V σ[R/α] j } V 1 j def = {((∅ | ), (∅ | ))} V σ ⊗ σ j def = {((s1 + + s 1 | v1, v 1 ), (s2 + + s 2 | v2, v 2 )) | ((s1 | v1), (s2 | v2)) ∈ V σ j ∧ ((s 1 | v 1 ), (s 2 | v 2 )) ∈ V σ j V σ σ j def = {((s1 | λ(x : σ ). e1), (s2 | λ(x : σ ). e2)) | ∀j ≤ j, s 1 , s 2 , ((s 1 | v1), (s 2 | v2)) ∈ V σ j . s 1 = s1 + + s 1 ∧ s 2 = s2 + + s 2 ⇒ ((s 1 | e1[v1/x]), (s 2 | e2[v2/x])) ∈ E σ j } V µα. σ j def = {((s1 | foldµα.σ v1), (s2 | foldµα.σ v2)) | ∀j < j.((s1 | v1), (s2 | v2)) ∈ V σ[µα. σ/α] j } V !σ j def = {((∅ | share(s1 : Ψ 1). v1), (∅ | share(s2 : Ψ 2). v2)) | ((s1 | v1), (s2 | v2)) ∈ V σ j } V Box 0 j def = {(([ 1 → •] | 1), ([ 2 → •] | 2))} V Box 1 σ j def = {(([ 1 → (s1 | v1)] | 1), ([ 2 → (s2 | v2)] | 2)) | ((s1 | v1), (s2 | v2)) ∈ V σ j } V [σ] j def = {((∅ | [v1]), (∅ | [v2])) | (v1, v2) ∈ V σ j } E σ j def = {(e1, e2) | ∀j ≤ j. e1 U → j v1 ⇒ ∃v2. e2 U → * v2 ∧ (v1, v2) ∈ V σ j-j } E σ j def = {((s1 | e1), (s2 | e2)) | ∀j ≤ j, (s 1 | v1).(s1 | e1) L → j (s 1 | v1) ⇒ ∃(s 2 | v2).(s2 | e2) L → * (s 2 | v2) ∧ ((s 1 | v1), (s 2 | v2)) ∈ V σ j-j }
Theorem 5 (Soundness of Logical Relation with respect to Contextual Equivalence) ( log ) ⊂ ( ctx ).

Hybrid program examples

In-Place Transformations

In Section 2.2 (Linear Memory in λ L ) we proposed a program for in-place reversal of linear lists defined by the type LinList σ def = µα. 1 ⊕ Box 1 (σ ⊗ α). We can also define a type of ML lists List σ def = µα. 1 + σ × α. Note that ML lists are compatible with shared linear lists, in the sense that List σ !(LinList ![σ]). This enables writing in-place list-manipulation functions in λ L , and exposing them to beginners at a λ U type:

rev xs def = UL LinList ![σ] (share (rev_into copy ( LinList ![σ] LU(xs)) Nil))
This example is arguably silly, as the allocations that are avoided by doing an in-place traversal are paid when copying the shared list to obtain a uniquelyowned version. A better example of list operations that can profitably be sent on the linear side is quicksort, whose code we give in Figure 11 (Quicksort). An ML implementation allocates intermediary lists for each recursive call, while the surprisingly readable λ U implementation only allocates for the first copy.

Typestate Protocols

Linear types can enforce proper allocation and deallocation of resources, and in general any automata/typestate-like protocols on their usage by encoding the state transitions as linear transformations. In the simple example of file-descriptor handling in the introduction, additional safety compared to ML programming can be obtained by exposing file-handling functions on the λ U side, with linear types. We assumed the following API for linear file handling, which enforces a correct usage protocol:

Conclusion

In our proposed multi-language design, a simple linear type system mirroring the standard rules of intuitionistic linear logic can be equipped with linear state and usefully complement a general-purpose functional ML language, without breaking equational reasoning or parametricity-and without requiring a significantly more complex meta-theory.

Fine-grained language boundaries allow interesting programming patterns to emerge, and full abstraction provides a novel rigorous specification of what it means for multi-language design to avoid abstraction leaks from advanced features into the general-purpose or beginner-friendly languages.

Related Work

Having a stack of usable, interoperable languages, extensions or dialects is at the forefront of the Racket approach to programming environments, in particular for teaching [START_REF] Felleisen | The teachscheme! project: Computing and programming for every student[END_REF].

Our multi-language semantics builds on the seminal work by [START_REF] Matthews | Operational semantics for multilanguage programs[END_REF], who gave a formal semantics of interoperability between a dynamically and a statically typed language. Others have followed the Matthews-Findler approach of designing multi-language systems with fine-grained boundaries-for instance, formalizing interoperability between a simply and dependently typed language [START_REF] Osera | Dependent interoperability[END_REF]; between a functional and typed assembly language [START_REF] Patterson | Fun-TAL: Reasonably mixing a functional language with assembly[END_REF]; between an ML-like and an affinely typed language, where linearity is enforced at runtime on the ML side using stateful contracts [START_REF] Tov | Stateful contracts for affine types[END_REF]; and between the source and target languages of compilation to specify compiler correctness [Perconti and [START_REF] James | Verifying an open compiler using multilanguage semantics[END_REF]. However, all these papers address only the question of soundness of the multi-language; we propose a formal treatment of usability and absence of abstraction leaks.

The only work to establish that a language embeds into a multi-language in a fully abstract way is the work on fully abstract compilation by Ahmed and Blume [2011] and New, Bowman, and [START_REF] New | Fully abstract compilation via universal embedding[END_REF] who show that their compiler's source language embeds into their source-target multi-language in a fully abstract way. But the focus of this work was on fully abstract compilation, not on usability of user-facing languages.

The Eco project [START_REF] Barrett | Finegrained language composition: A case study[END_REF]] is studying multi-language systems where user-exposed languages are combined in a very fine-grained way; it is closely related in that it studies the user experience in a multi-language system. The choice of an existing dynamic language creates delicate interoperability issues (conflicting variable scoping rules, etc.) as well as performance challenges. We propose a different approach, to design new multilanguages from scratch with interoperability in mind to avoid legacy obstacles.

We are not aware of existing systems exploiting the simple idea of using promotion to capture uniquely-owned state and dereliction to copy it-common formulations would rather perform copies on the contraction rule.

The general idea that linear types can permit reuse of unused allocated cells is not new. In [START_REF] Wadler | Linear Types Can Change the World! In Programming Concepts and Methods[END_REF], a system is proposed with both linear and non-linear types to attack precisely this problem. It is however more distant from standard linear logic and somewhat ad-hoc; for example, there is no way to permanently turn a uniquely-owned value into a shared value, it provides instead a local borrowing construction that comes with ad-hoc restrictions necessary for safety. (The inability to give up unique ownership, which is essential in our list-programming examples, seems to also be missing from Rust, where one would need to perform a costly operation of traversing the graph of the value to turn all pointers into Arc nodes.)

The RAML project [START_REF] Hoffmann | Resource Aware ML[END_REF]] also combines linear logic and memory reuse: its destructive match operator will implicitly reuse consumed cells in new allocations occurring within the match body. Multilanguages give us the option to explore more explicit, flexible representations of those low-level concern, without imposing the complexity to all programmers.

A recent related work is the Cogent language [O'Connor, Chen, Rizkallah, Amani, Lim, Murray, Nagashima, Sewell, and Klein, 2016], in which linear state is also viewed as both functional and imperative -the latter view enabling memory reuse. The language design is interestingly reversed: in Cogent, the linear layer is the simple language that everyone uses, and the non-linear language is a complex but powerful language that is used when one really has to, named C.

Our linear language λ L is sensibly simpler, and in several ways less expressive, than advanced programming languages based on linear logic [START_REF] Tov | Practical affine types[END_REF], separation logic [START_REF] Balabonski | The design and formalization of Mezzo, a permission-based programming language[END_REF], fine-grained permissions [Garcia, Tanter, Wolff, and Aldrich, 2014]: it is not designed to stand on its own, but to serve as a useful side-kick to a functional language, allowing safer resource handling.

One major simplification of our design compared to more advanced linear or separation-logic-based languages is that we do not separate physical locations from the logical capability/permission to access them (e.g., as in [START_REF] Ahmed | L3 : A linear language with locations[END_REF]). This restricts expressiveness in well-understood ways [START_REF] Fahndrich | Adoption and focus: Practical linear types for imperative programming[END_REF]: shared values cannot point to linear values.

Alms [START_REF] Tov | Practical affine types[END_REF], Quill [START_REF] Morris | The best of both worlds: Linear functional programming without compromise[END_REF] and Linear Haskell [Bernardy, Boespflug, Newton, Jones, and Spiwack, 2018] add linear types to a functional language, trying hard not to lose desirable usability property, such as type inference or the genericity of polymorphic higher-order functions. This is very challenging; for example, Linear Haskell gives up on principality of inference7 . Our multilanguage design side-steps this issue as the general-purpose language remains unchanged. Language boundaries are more rigid than an ideal no-compromise language, as they force users to preserve the distinction between the generalpurpose and the advanced features; it is precisely this compromise that gives a design of reduced complexity.

Finally, on the side of the semantics, our system is related to LNL [Benton, 1994], a calculus for linear logic that, in a sense, is itself built as a multi-language system where (non-duplicable) linear types and (duplicable) intuitionistic types interact through a boundary. It is not surprising that our design contains an instance of this adjunction: for any σ there is a unique σ such that σ !σ, and converting a σ value to this σ and back gives a !σ and is provably equivalent, by boundary cancellation, to just using share .

A Logical relation

To define the logical relation in a precise way, we introduce a new grammar of "relational types" ρ, ρ, that simply extend the grammar of σ, σ to include a case for a relation on λ U types (R, σ 1 , σ 2 ).

Introducing this lightweight syntax for relations here is a middle way between definitions that use an explicit relational substitution (cluttering the relation with yet another index) and a full-blown logic for parametricity as in Plotkin and Abadi [1993] ρ ::= . . . all cases for σ, but using ρ, ρ recursively | (R, σ1, σ2) ρ ::= all cases for σ, but using ρ, ρ recursively Every ρ has two associated types, the types of terms that it relates, which we denote (ρ) 1 , (ρ) 2 . It is defined as follows: First, we define when closed values are related at each type, indexing by a natural number to break the circularity of recursive types. The relations are defined by nested induction on j, ρ, ρ, any time a bigger type is used in a definition, the step-index j is decremented.

The definition of E σ j shows that this is an assymetric relation capturing a notion of approximation, not equivalence.

Next, we extend the relations to open terms by defining open terms to be related when they are related when closed by related substitutions.

The Fundamental Property is the key to proving parametricity results.

Lemma 11 (Fundamental Property) Finally, we prove our logical relation is sound with respect to contextual equivalence, that is, it can be used as a more tractible way to prove contextual equivalence results, such as lump/unlump cancellation.

Theorem 6 (Soundness of Logical Relation) log ⊂ ctx

The proof is by induction on contexts, showing that every term formation rule preserves logical relatedness. These "compatibility" lemmas are extensive, but their proofs are simple. Their proofs are in the extended technical report.

  let concat_lines path : String = UL( loop (open LU(path)) LU(Nil) where rec loop handle LU(acc : List String) = match line handle with | Next line LU(handle) -> loop handle LU(Cons line acc) | EOF handle -> close handle; LU(rev_concat "\n" acc))

  Expr. e ::= x | e1, e2 | π1 e | π2 e | | e1; e2 | λ(x : σ). e | e1 e2 | inj i e | case e of x1. e1 | x2. e2 | foldµα.σ e | unfold e | Λα. e | e [σ]

Fig. 1 .Fig. 2 .

 12 Fig. 1. Unrestricted Language: Syntax

Fig. 3 .

 3 Fig. 3. Linear Language: Surface Syntax

Fig. 4 .

 4 Fig. 4. Linear Language: Surface Static Semantics

  Expressions e + ::= • • • | | share(s : Ψ ). e with share e def = share(∅ : •). e Values v + ::

  s | e; e : σ Ψ ; Γ , x : σ l s | e : σ Ψ ; Γ l s | λ(x : σ). e : σ σ Ψ ; Γ l s | e : σ σ Ψ ; Γ l s | e : σ Ψ Ψ ; Γ Γ l s + + s | e e : σ Ψ ; Γ l s | e : σi Ψ ; Γ l s | inj i e : σ1 ⊕ σ2

Fig. 5 .

 5 Fig. 5. Linear Language: Internal Static Semantics

  e) L (s | e ) let x1, x2 = v1, v2 in e L e[v1/x1][v2/x2] ; e L e (λ(x : σ). e) v L e[v/x]

Theorem 1 (

 1 Progress) If Ψ ; Γ l s | e : σ, then either e is a value v or there exists (s | e ) such that (s | e) L → (s | e ).

Lemma 6 (

 6 Context decomposition) If Ψ ; Γ l s | K[ : σ] : σ holds, then Ψ ; Γ l s | K[e] : σ holds if and only if there exists Ψ , Γ , s such that Ψ = Ψ Ψ , Γ = Γ Γ , s = s + + s and Ψ ; Γ l s | e : σ. Theorem 2 (Subject reduction for λ L ) If Ψ ; Γ l s | e : σ and (s | e) L → (s | e ), then there exists a (unique) Ψ such that Ψ ; Γ l s | e : σ.

  Expressions e | e e + ::= • • • | UL(s : Ψ | e) with UL(e) def = UL(∅ : • | e) e + ::= • • • | LU(e) Contexts Γ ::= • | Γ , x : σ | Γ , α | Γ , x : σ Typing rules Γ lu e : σ Ψ | Γ ul s | e : σ with Γ ul e : σ def = • | Γ ul ∅ | e : σ (Typing rules of Γ u e : σ reused, with mixed context !Γ ) (Typing rules of Ψ ; Γ l s | e : σ reused, with mixed context Γ ) !Γ lu e : σ • | !Γ ul ∅ | LU(e) : ![σ] Ψ | !Γ ul s | e : ![σ] !Γ lu UL(s : Ψ | e) : σ Reduction rules (Reduction rules of λ U and λ L reused unchanged) e

Fig. 7 .

 7 Fig. 7. Multi-language: Lump and Boundaries

def=Fig. 8 .

 8 Fig. 8. Multi-language: Static Interoperability Semantics

Lemma 9 (

 9 Substitution of polymorphic variables) If Σ ul σ σ and α / ∈ Σ, then Σ ul σ[σ /α] σ[σ /α] and their lumping operations coincide on all values.

Definition 1 (

 1 Contextual equivalence in λ U ) We say that e, e such that Γ u e, e : σ are contextually equivalent, written e ≈ ctx u e , if, for any expression context C[ ] such that • u C[e] : 1, the closed terms C[e] and C[e ] are equi-terminating. Definition 2 (Contextual equivalence in λ UL ) We say that e, e such that Γ lu e, e : σ are contextually equivalent, written e ≈ ctx lu e , if, for any expression context C[ ] such that • lu C[e] : 1, the closed terms C[e] and C[e ] are equiterminating.

Fig. 10 .

 10 Fig. 10. Multi-language Logical Relation (excerpt)

  Fig. 11. Quicksort

Fig. 12 .

 12 Fig. 12. Relation Type Syntax

1.U→ 2 |

 2 Fig. 13. Logical Approximation for Closed Terms

Fig. 14 .

 14 Fig. 14. Logical Approximation for Open Terms

https://caml.inria.fr/pub/docs/u3-ocaml/ocaml-ml.html

http://www.scala-lang.org/old/node/8610

The unrestricted language λ U is a run-of-the-mill idealized ML language with functions, pairs, sums, iso-recursive types and polymorphism. It is presented in its explicitly typed form-we will not discuss type inference in this work. The full syntax is described in Figure1, and the typing rules in Figure2. The dynamic semantics is completely standard. Having binary sums, binary products and iso-recursive types lets us express algebraic datatypes in the usual way. Γ u e : σ x : σ ∈ Γ Γ u x : σ Γ u : 1 Γ u e : 1 Γ u e : σ Γ u e; e : σ Γ u e1 : σ1 Γ u e2 : σ2 Γ u e1, e2 : σ1 × σ2 Γ u e : σ1 × σ2 Γ u π i e : σi Γ , x : σ u e : σ Γ u λ(x : σ). e : σ → σ Γ u e : σ → σ Γ u e : σ Γ u e e : σ Γ u e : σi Γ u inj i e : σ1 + σ2 Γ u e : σ1 + σ2 Γ , x1 : σ1 u e1 : σ Γ , x2 : σ2 u e2 : σ Γ u case e of x1. e1 | x2. e2 : σ Γ u e : σ[µα. σ/α] Γ u foldµα.σ e : µα. σ Γ u e : µα. σ Γ u unfold e : σ[µα. σ/α] Γ , α u v : σ Γ u Λα. v : ∀α. σ Γ u e : ∀α. σ

Γ 1 (Γ 2, x : σ) def = (Γ 1 Γ 2), x : σ (x / ∈ Γ 1) Γ l e : σ !Γ , x : σ l x : σ Γ 1 l e1 : σ1 Γ 2 l e2 : σ2 Γ 1 Γ 2 l e1, e2 : σ1 ⊗ σ2 Γ l e : σ1 ⊗ σ2 Γ , x1 : σ1, x2 : σ2 l e : σ Γ Γ l let x1, x2 = ein e : σ !Γ l : 1 Γ l e : 1 Γ l e : σ Γ Γ l e; e : σ Γ , x : σ l e : σ Γ l λ(x : σ). e : σ σ Γ l e : σ σ Γ l e : σ Γ Γ l e e : σ Γ l e : σi Γ l inj i e : σ1 ⊕ σ2 Γ l e : σ1 ⊕ σ2 Γ , x1 : σ1 l e1 : σ Γ , x2 : σ2 l e2 : σ

Standard presentations of linear logic force contexts to be completely distinct, but have a separate rule to duplicate linear variables, which is less natural for programming.

Thanks to Stephen Dolan for pointing out that λf.λx. f x has several incompatible Linear Haskell types.

Acknowledgments

We thank our anonymous reviewers for their feedback, as well as Neelakantan Krishnaswami, François Pottier, Jennifer Paykin, Sylvie Boldo and Simon Peyton-Jones for our discussions on this work.

This work was supported in part by the National Science Foundation under grants CCF-1422133 and CCF-1453796, and the European Research Council under ERC Starting Grant SECOMP (715753). Any opinions, findings, and conclusions expressed in this material are those of the authors and do not necessarily reflect the views of our funding agencies.