{'fraction_non_alphanumeric': 0.03740040913006029, 'fraction_numerical': 0.006056201550387597, 'mean_word_length': 4.452777573934101, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 4, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Direct Foundations for Compositional Programming

The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+. The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of Fi+ does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of Fi+ based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full Fi+ calculus. Unlike the elaboration semantics, which gives the semantics to Fi+ indirectly via a target language, the TDOS approach gives a semantics to Fi+ directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the Fi+ calculus and all its proofs in the Coq proof assistant.


Introduction
Compositional Programming [46] is a recently proposed modular programming paradigm. It offers a natural solution to the Expression Problem [42] and novel approaches to modular pattern matching and dependency injection. The CP language adopts Compositional Programming. In CP, several new programming language constructs enable Compositional Programming. Of particular interest for this paper, CP has a notion of typed first-class traits [5], which are extended in CP to also enable a form of family polymorphism [16].
The semantics of CP and its notion of traits is defined via an elaboration to the core calculus F + i [7]: a polymorphic core language with a merge operator [34] and disjoint intersection types [30]. The elaboration of traits is inspired by Cook's denotational semantics of inheritance [12]. In the denotational semantics of inheritance, the key idea is that mechanisms such as classes or traits, which support self-references (a.k.a. the this keyword in conventional OOP languages), can be modeled via open recursion. In other words, the encoding of classes or traits is parametrized by a self-reference. This allows late binding of selfreferences at the point of instantiation and enables the modification and composition of traits before instantiation. Instantiation happens when new is used, just as in conventional OOP languages. When new is used, it essentially closes the recursion by binding the self-reference, which then becomes a recursive reference to the instantiated object. In the denotational semantics of inheritance, new is just a fixpoint operator.
The semantics of the original formulation of F + i [7] itself is also given by an elaboration into F co , a System F-like language with products. Unlike F + i , F co has no subtyping or intersection types, and it has a conventional operational semantics. The main reason for F + i to use elaboration is that F + i has a type-dependent semantics: types may affect the runtime behavior of a program. The elaboration semantics for F + i seems like a natural choice, since this is commonly seen in various other type-dependent languages and calculi. For instance, the semantics of type-dependent languages with type classes [43], Scala-style implicits [29] or gradual typing [40] all usually adopt an elaboration approach. In contrast, in the past, more conventional direct formulations using an operational semantics have been avoided for languages with a type-dependent semantics. The appeals of the elaboration semantics are simple type-safety proofs, and the fact that they directly offer an implementation technique over conventional languages without a type-dependent semantics.
There are also important drawbacks when using an elaboration semantics. One of them is simply that more infrastructure is needed for a target language (such as F co ) and its associated semantics and metatheory. Moreover, the elaboration semantics is indirect, and to understand the semantics of a program, we must first translate it to the target language (which may be significantly different from the source) and then reason in terms of the target. More importantly, besides type-safety, another property that is often desirable for an elaboration semantics is coherence [35]. Many elaboration semantics are non-deterministic: the same source program can elaborate into different target programs. If those different programs have a different semantics, then this is problematic, as it would imply that the source language would have a non-deterministic or ambiguous semantics. Coherence ensures that even if the same program elaborates to different target expressions, the different target expressions are semantically equivalent, eventually evaluating to the same result.
For some languages, including F + i , proving coherence is highly non-trivial and hard to scale to common programming language features. For the original F + i , the proof of coherence comes at the cost of simple features such as recursion and impredicative polymorphism. The proof of coherence for F + i is based on a logical relation called canonicity [6]. Together with a notion of contextual equivalence, the two techniques are used to prove coherence. The use of logical relations is a source of complexity in the proof and the reason why recursion and impredicative polymorphism have not been supported. For recursion, in principle, the use of a more sophisticated step-indexed logical relation [3] may enable a proof of coherence, at the cost of some additional complexity. However, due to the extra complexity, this was left for future work. For impredicative polymorphism, Bi et al. [7] identified important technical challenges, and it is not known if the proof can be extended with such a feature. The absence of recursion and impredicative polymorphism creates a gap between theory and practice, since CP fundamentally relies on them. Moreover, the proofs of correctness of CP rely on the assumption that F + i with recursion and impredicative polymorphism would preserve all the properties of F + i . Impredicative polymorphism is needed in CP to allow the types of traits with polymorphic methods to be used as type parameters for other polymorphic functions. Recursion is needed in CP because the denotational semantics uses fixpoint operators to instantiate traits. In addition, the fixpoint operators must be lazy; otherwise, self-references can easily trigger non-termination. Therefore, a call-by-name (CBN) semantics is more natural and also assumed in the CP encoding of traits. However, the semantics of the F co calculus is call-by-value (CBV) and, by inheritance, the elaboration semantics of F + i has a CBV semantics as well. This paper presents a new formulation of F + i based on a type-directed operational semantics (TDOS) [20]. The TDOS approach has recently been proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Although F + i is not a new calculus, we revise its formulation significantly in this paper. Our new formulation of F + i is different from the original one in three aspects. Firstly, the semantics of the original F + i is given by elaborating to F co , while our semantics for F + i is a direct operational semantics. Secondly, our new formulation of F + i supports recursion and impredicative polymorphism. Finally, we employ a call-by-name evaluation strategy.
Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the complete F + i calculus with recursion and impredicative polymorphism. Moreover, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism uses only simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. Thus, this removes the gap between theory and practice and validates the original proofs of correctness for the CP language. Figure 1 contrasts the differences in terms of proofs and implementation of CP using Zhang et al.'s original work and our own work. We formalized the TDOS variant of the F + i calculus, together with its type-soundness and determinism proof in the Coq proof assistant. Moreover, we have a new implementation of CP based on our new reformulation of F + i . In summary, the contributions of this work are: CBN F + i with recursion and impredicative polymorphism. This paper presents a CBN variant of F + i extended with recursion and impredicative polymorphism. Determinism and type-soundness for F + i using a TDOS. We prove the typesoundness and determinism of F + i using a direct TDOS. These proofs validate the proofs of correctness previously presented for CP by Zhang et al. [46]. Technical innovations. Our formulation of F + i has various technical innovations over the original one, including a new formulation of subtyping using splittable types [22] and more flexible term applications. Implementation and Mechanical formalization. We formalized the TDOS variant of the F + i calculus, together with its type-soundness and determinism proof in the Coq proof assistant. We also have a new implementation of CP built on top of a TDOS formulation of F + i available at https://plground.org. The full Coq formalization is available at: https://github.com/andongfan/CP-Foundations

Motivations and Technical Innovations
In this section, we introduce Compositional Programming by example and show how CP traits elaborate to F + i expressions. After that, we will discuss the practical issues that motivate us to reformulate F + i , as well as technical challenges and innovations.

Compositional Programming by Example
To demonstrate the capabilities of Compositional Programming, we show how to solve a variant of the Expression Problem [42] in the CP language. Our solution is adapted from the original one by Zhang et al. [46]. In this variant, in addition to the usual challenge of extensibility in multiple directions, we also consider the problem of context evolution [25,37], so the interpreter may require different contextual information for different features of the interpreter. The CP language allows a modular solution to both challenges, which also illustrates some key features in Compositional Programming, including first-class traits [5], nested composition [6], and disjoint polymorphism [2]. Examples are based on a simple expression language, and the goal is to perform various operations over it, such as evaluation and free variable bookkeeping. The expression language consists of numbers, addition, variables, and let-bindings. Besides CP code, we also provide analogous Haskell code in the initial examples so that readers can connect them with existing concepts in functional languages.
Compositional interfaces. First, we define the compositional interface for numeric literals and addition. The compositional interface at the top of Figure 2a is similar to Haskell's algebraic data type at the top of Figure 2b. Exp is a special kind of type parameter in CP called a sort, which serves as the return type of both constructors Lit and Add. Sorts will be instantiated with concrete representations later. Internally, sorts are handled differently from normal type parameters [46]. In accordance with the compositional interface, we can then define how to evaluate the expression language.
Polymorphic contexts. As shown in the middle of Figure 2a, the type Eval declares a method eval that takes a context and returns an integer. Ctx is a type parameter that can be instantiated later, enabling particular traits to assume particular contextual information for the needs of various features. The technique is called polymorphic contexts [46] in Compositional Programming.  Compositional traits. The trait evalNum in Figure 2a is parametrized by a type parameter Ctx. Note that, in CP, type parameters always start with a capital letter, while regular parameters are lowercase. The trait evalNum implements the compositional interface NumSig by instantiating it with the sort Eval Ctx. Traits are the basic reusable unit in CP, which are usually type-checked against compositional interfaces. In this trait, we use a lightweight syntax called method patterns to define how to evaluate different expressions. Such a definition is analogous to pattern matching in Figure 2b. Since Lit and Add do not need to be conscious of any information in the context, the type parameter Ctx is unconstrained. The only thing that we can do to the polymorphic context is either to ignore it (like in Lit) or pass it to recursive calls (like in Add).

More expressions.
Adding more constructs to the expression language is awkward in Haskell because algebraic data types are closed. However, language components can be modularly declared in CP. Two new constructors, Let and Var, are declared in the second compositional interface VarSig, as shown in Figure 3. Then the two traits implement VarSig using method patterns for the new constructors. Since the two new expressions need to inspect or update some information in the context, we expose the appropriate Env part to evalVar, while the remaining context is kept polymorphic. This is achieved with the disjointness constraint [2] Ctx*Env in evalVar. A disjointness constraint denotes that the type parameter Ctx is disjoint to the type Env  type Env. Also note that the notation { ctx with env = ... } denotes a polymorphic record update [9]. In the code for let-expressions, we need to update the environment in the recursive calls to extend it with a new entry for the let-variable.
Intersection types. Independently defined interfaces can be composed using intersection types. For example, ExpSig below is an intersection of NumSig and VarSig, containing all of the four constructors: More operations. Not only can expressions be modularly extended, but we can easily add more operations. In Figure 4, a new trait fv modularly implements a new operation that records free variables in an expression. Here, union and delete are two library functions for arrays. The modular definition of fv is quite natural in functional programming, but it is hard in traditional object-oriented programming. We have to modify the existing class definitions and supplement them with a method. This is typical of the well-known Expression Problem. In summary, we have shown that Compositional Programming can solve both dimensions of this problem: adding expressions and operations.

Dependency injection.
Besides the Expression Problem, Figure 4 also shows another significant feature of CP: dependency injection. In evalWithFV, a new implementation of evaluation is defined with a dependency on free variables. The method pattern for Let will check if s appears as a free variable in e2. If so, it evaluates e1 first as usual; otherwise, we do not need to do any computation or update the environment since s is not used at all. Note that the compositional interface ExpSig is instantiated with two types separated by a fat arrow (⇒) (⇒ was originally denoted by % in Zhang et al.'s implementation of CP). FV on the left-hand side is the dependency of evalWithFV. In other words, the definition of evalWithFV depends on another trait that implements ExpSig<FV>. The static type checker of CP will check this fact later at the point of trait instantiation. With such dependency injection, we can call e2.fv even if evalWithFV does not have an implementation of fv. In other words, evalWithFV depends only on the interface of fv (the type FV), but not any concrete implementation.
Self-type annotations. Before we show how to perform the new version of the evaluation over the whole expression language, we want to create a repository of expressions for later use. We expect that these expressions are unaware of any concrete operation, so we use a polymorphic Exp type to denote some abstract type of expressions. The code that creates the repository of expressions is 1 : x" (Lit 4) (Let "y" (Lit 8) (Add (Var "x") (Var "y"))); }; To make constructors available from the compositional interface, we add a self-type annotation to the trait repo. The self type annotation [self : ExpSig<Exp>] imposes a requirement that the repo should finally be merged with some trait implementing ExpSig<Exp>. This requirement is also statically enforced by the static type checker of CP. This is the second mechanism in Compositional Programming to modularly inject dependencies.

Nested trait composition.
With the language components ready, we can compose them using the merge operator [14], which in the CP language is denoted as a single comma (,). First, we show how to compose the old version of the evaluation: exp = new repo @(Eval Env) , evalNum @Env , evalVar @Top; exp.var.eval { env = empty } --> 12 Since the context has evolved after we add variables, we pass different type arguments to the two traits to make the final context consistent. The final context type is Env, so we pass Env to evalNum and Top to evalVar. Type arguments are prefixed by @ in CP. A more interesting example is to merge the new version of evaluation with free variable bookkeeping: After the trait composition, both operations (eval and fv) are available for expressions that are built with the four constructors (Lit, Add, Let, and Var). Note that here fv satisfies the dependency of evalWithFV. If no implementation of the type FV is present in the composition, there would be a type error, since the requirement for evalWithFV would not be satisfied. The composition of the three traits is nested because the two methods nested in the four constructors are composed, as visualized in Figure 5. With nested trait composition, the Expression Problem is elegantly solved in Compositional Programming. Moreover, we allow context evolution using a relatively simple way with polymorphic contexts. Impredicative polymorphism. Another feature of CP is that it allows the creation of objects with polymorphic methods, similar to most OOP languages with generics where classes can contain polymorphic methods (like Java). However, for this to work properly, CP must support impredicative polymorphism (the ability to instantiate type parameters with polymorphic types) as System F does. For example, consider:  While accepted by our variant of CP and F + i , such polymorphic instantiations are forbidden in the original formulation of F + i .

Elaborating CP to F
Under the surface of CP, the foundation for Compositional Programming is the F + i calculus. We present the key features in F + i and take a closer look at the connection between CP and F + i expressions. Here we focus on the elaboration of traits, which are the most important aspect of this paper. We refer curious readers to the work by Zhang et al. [46] for the full formulation of the type-directed elaboration of CP.
Key features of the F + i calculus. F + i is basically a variant of System F [17,33] extended with intersection types and a merge operator. In the F + i calculus, we denote the merge operator with a double comma (, ,) (instead of the single comma notation in CP), following the original notation proposed by Dunfield [14]. The merge operator allows us to introduce terms of intersection types. For example, 1 , , true is a term of type Int & Bool. Moreover, record concatenation, which is used to encode multi-field traits, is encoded as merges of records in F + i . Thus, multi-field records are represented as merges of multiple single-field records. However, to ensure determinism of operational semantics, not all terms can be merged with each other. We impose a disjointness check when typing merges: a merge can only type check when the types of the terms being merged are disjoint. It ensures that every part in a merge can be distinguished by its type. For traits, for example, the disjointness restriction ensures that traits cannot have two fields/methods with the same name m and overlapping types, which could otherwise lead to ambiguity when doing method lookup. Here, we show an example of ambiguity if there is no disjointness check. With intersection types, both A & B ≤ A and A & B ≤ B are valid. Therefore, a merge 1 , , 2 of type Int & Int can be typed with Int, but at runtime, two different values of type Int are found. Thus, an expression such as (1 , , 2) + 1 could evaluate to either 2 or 3. Since we wish for a deterministic semantics, we use disjointness to prevent such forms of ambiguity. On the other hand, (1 , , true) + 1 type checks because Int and Bool are disjoint, and it evaluates to 2 unambiguously. A disjointness constraint can also be added to a type variable in a System F-style polymorphic type, such as ∀X * Int. X & Int. Moreover, to support unrestricted intersection types like Int & Int, the disjointness check is relaxed to consistency for certain terms, so that merges with duplications like 1 , , 1 are allowed.

Elaborating traits into F +
i . The elaboration of traits is inspired by Cook's denotational semantics of inheritance [12]. To use a concrete example, we revisit the trait repo defined in Section 2. The CP code above is elaborated to corresponding F + i code of the form: The type parameter Exp in the repo trait is expressed by a System F-style type lambda (ΛA. e). Note that CP employs a form of syntactic sugar for constructors to allow concise use of constructors and avoid explicit uses of new. The source code Add (Lit 4) (Lit 8) is first expanded into new $Add (new $Lit 4) (new $Lit 8), which insert new operators. Next we describe the elaboration process of creating and instantiating traits: Creation of traits: A trait is elaborated to a generator function whose parameter is a self-reference (like self above) and whose body is a record of methods;

Instantiation of traits:
The new construct is used to instantiate a trait. Uses of new are elaborated to a fixpoint which applies the elaborated trait function to a self-reference.
In the definition of the field num there are three elaborations of new. For instance, the CP code new $Lit 4 corresponds to the F + i code fix self:Exp. $Lit 4 self.
It is clear now that our trait encoding is heavily dependent on recursion, due to the self-references employed by the encoding. However, the original F + i [7] does not support recursion, which reveals a gap between theory and practice.

The Gap Between Theory and Practice
Our primary motivation to reformulate F + i is to bridge the gap between theory and practice. The original formulation of F + i lacks recursion, impredicative polymorphism and uses the traditional call-by-value (CBV) evaluation strategy. However, the recent work of CP assumes a different variant of F + i that is equipped with fixpoints and the call-by-name (CBN) evaluation. It is worthwhile to probe into the causes of such differences.

Non-triviality of coherence.
Recursion is essential for general-purpose computation in programming. More importantly, our encoding of traits requires recursion. For example, new e is elaborated to fix self. e self. However, adding recursion to the original version of F + i turns out to be highly non-trivial. The original F + i is defined using an elaboration semantics. A fundamental property of F + i is coherence [35], which states that the semantics is unambiguous. Coherence is non-trivial due to the presence of the merge operator [14]. To prove coherence, a logical relation, called canonicity [7], is used to reason about contextual equivalence in the original work of F + i . For example, with contextual equivalence, we can show that the two possible elaborations for the same F + i source expression into F co are contextually equivalent: Two typing derivations lead to two elaborations in this example, which pick different sides of the merge. However, both elaborated expressions will be reduced to 1 eventually.
Unfortunately, the proof technique for coherence based on logical relations does not immediately scale to recursive programs and programs with impredicative polymorphism. A possible solution, known from the research of logical relations, is to move to a more sophisticated step-indexed form of logical relations [1]. However, this requires a major reformulation of the proofs and metatheory of the original F + i , and it is not clear whether additional challenges would be present in such an extension. Thus, the lack of the two features in the theory of the original F + i remains a serious limitation since only terminating programs and predicative polymorphism are considered. In other words, we cannot encode traits as presented in Section 2.2 in the original F + i . To get around this issue and enable the encoding of traits, Zhang et al. [46] simply assumed an extension of F + i with recursion and their proof of coherence for CP was done under the assumption that the original F + i with recursion was coherent or deterministic.
Our work rectifies this gap in the theory of Compositional Programming and the CP language. We reformulate F + i using a direct type-directed operational semantics [22] that allows recursion and prove that the semantics is deterministic. Thus, our reformulation of F + i can serve as a target language to encode traits and validate the proofs of the elaboration of CP in terms of F + i with recursion. In addition, our approach gives a semantics to F + i directly, instead of relying on an indirect elaboration semantics to a System F-like language.
Evaluation strategies. Most mainstream programming languages use CBV, but CBN is a more natural evaluation strategy for object encodings such as Cook's denotational semantics of inheritance. As stated by Bruce et al. in their work on object encodings [8]:

"Although we shall perform conversion steps in whatever order is convenient for the sake of examples, we could just as well impose a call-by-name reduction strategy. (Most of the examples would diverge under a call-by-value strategy. This can be repaired at the cost of some extra lambda abstractions and applications to delay evaluation at appropriate points.)"
In our elaboration of traits, we adopt a similar approach to object encodings. For example, consider the following CP expression: which is elaborated to the following (slightly simplified) F + i expression: The trait expression is elaborated to a function, and the new expression turns the function into a fixpoint. Unfortunately, this expression terminates under CBN but diverges under CBV. If evaluated under CBV, the variable self will be evaluated repeatedly, despite the fact that only self .l 1 is used: We may tackle the problem of non-termination by wrapping self-references in thunks, but CBN provides a simpler and more natural way. In our CBN formulation of F + i , {l = e} is already a value (instead of {l = v}), so we do not need to further evaluate e: The l 2 field is further evaluated only when a record projection is performed: This example illustrates how our new CBN formulation of F + i avoids non-termination of trait instantiation.

Technical Challenges and Innovations
The main novelty of our reformulation of F + i is the use of a type-directed operational semantics [20] instead of an elaboration semantics. With a TDOS, adding recursion and impredicative polymorphism to our proof of determinism is trivial. Our work is an extension of the λ + i calculus [22] which adapts the TDOS approach. We also follow the subtyping algorithm design in λ + i . While λ + i supports BCD-style distributive subtyping [4], the addition of disjoint polymorphism does bring some technical challenges. Moreover, there are some smaller changes to F + i that enable us to type-check more programs and improve the design of the original F + i . We will give an overview of the technical challenges and innovations next. The role of casting. A merge like 1 , , true has multiple meanings under different types (e.g. Int or Bool). Eventually, we have to extract some components via the elimination of merges, which is a key issue when designing a direct operational semantics for a calculus with the merge operator. A non-deterministic semantics could allow e 1 , , e 2 → e 1 and e 1 , , e 2 → e 2 without any constraints, at the cost of losing both type preservation and determinism [14]. To obtain a non-ambiguous and type-safe semantics, we follow the TDOS approach [20]: which uses (up)casts to ensure that values have the right form during reduction. In a TDOS, there is a casting relation, which is used in the reduction rule for annotated values: Step-annov Casting enables us to drop certain parts from a term (e.g., 1 , , true → Int 1). Very often, it is necessary for us to do so to satisfy the disjointness constraint. Consider a function λx : Int. x , , false. For its body to be well-typed, x cannot contain a boolean. Hence, when the function is applied to 1 , , true, we cannot directly substitute the argument in. Instead, it is wrapped by (and later cast to) Int to resolve the potential conflict.
TDOS and function annotations. In casting, values in a merge are selected based on type information. In the absence of runtime type-checking, we need to know the type of input value syntactically to match it with the target type. Thus, functions must be accompanied by type annotations. The previous work λ + i [22] defines the syntax of functions like λx. e : A → C . While the original argument type A is always kept during reduction, λ + i 's casting relation may generate a value that has a proper subtype of the requested type: We make casting more precise with a more liberal syntax in F + i . We allow bare abstractions λx : A. e while λ + i does not. Our casting relation requires lambdas to be annotated (λx : A. e) : B, but the full annotation B does not have to be a function type. For example, (λx : Int. x , , true) : (Int → Int) & (Int → Bool) still acts as a function, and is equivalent to (λx : Algorithmic subtyping with disjoint polymorphism. F + i extends BCD-style distributive subtyping [4] to disjoint polymorphism. ∀X * Int. X & Int represents the intersection of some type X and Int assuming X is disjoint to Int. Like arrows or records, such universal types distribute over intersections. Hence, A well-known challenge in supporting distributivity in the BCD-style subtyping is to obtain an algorithmic formulation of subtyping. There have been many efforts to eliminate the explicit transitivity rule to obtain an algorithmic formulation [26,31,39]. Compared with the original F + i [7], we employ a different subtyping algorithm design, using splittable types [21]. This approach employs a type-splitting operation (B A C ) that converts a given type A to an equivalent intersection type The subtyping algorithm uses type splitting whenever an intersection type is expected in the conventional algorithm for subtyping without distributivity, and therefore handles distributivity smoothly and modularly.
Enhanced subtyping and disjointness with more top-like types. Unlike previous systems with disjoint polymorphism [2,7], we add a context in subtyping judgments to track the disjointness assumption X * A whenever we open a universal type ∀X * A. B, similar to the subtyping with F-bounded quantification. The extra information enhances our subtyping: we know a type must be a supertype of Top, if it is disjoint with Bot. This also fixes the following broken property in the original F + i , as we now have more types that are top-like.

Definition 2.1 (Disjointness specification). If A is disjoint with B, any common supertypes they have must be equivalent to Top.
Keeping this property is necessary for us to obtain a deterministic operational semantics. Meanwhile, we prove our subtyping and disjointness relations are decidable in Coq. Note that in the original F + i , the decidability of the two relations was proved manually, although the rest of the proof was mechanized.

The F + i Calculus and Its Operational Semantics
This section introduces the F + i calculus, including its static and dynamic semantics.

Syntax
The syntax of F + i is as follows: Term contexts Γ ::= · | Γ, x : A Type contexts ∆ ::= · | ∆, X * A Types. Types include the Top type and the uninhabited type Bot. Intersection types are created with A & B. Disjoint polymorphism, a key feature of F + i , is based on universal types with a disjointness quantifier ∀X * A. B, expressing that the type variable X is bound inside B and disjoint to type A. {l : A} denotes single-field record types, where l is the record label. Multi-field record types are desugared to intersections of single-field ones [36]: Expressions. As we will explain later with the typing rules, some expressions do not have an inferred type (or principal type), including lambda abstractions, type abstractions, and single-field records. We use metavariable p to represent these expressions, which with optional annotations, are values. Also, note that expressions inside record values do not have to be a value since our calculus employs call-by-name. The merge operator , , composes two expressions to make a term of an intersection type. The top value can be viewed as a merge of zero elements. Fixpoint expressions fix x : A. e construct recursive programs. The type annotation A denotes the type of x as well as the whole expression. Like record types, multi-field records are desugared to merges of single-field ones: . . . ; l n = e n } {l 1 = e 1 } , , . . . , , {l n = e n } Contexts. We have two contexts: Γ tracks the types of term variables; ∆ tracks the disjointness information of type variables, which follows the original design of F + i . We use ∆ A, ∆, and ∆ Γ judgments for the type well-formedness and the context wellformedness (defined in Appendix A.1). For multiple type well-formedness judgments, we combine them into one, i.e., ∆ A, B is equivalent to ∆ A ∧ ∆ B. Figure 6 shows our subtyping relation, which extends BCD-style subtyping [4] with disjoint polymorphism, records, and the bottom type. Compared with the original F + i , we add a context to track type variables and their disjointness information. The context not only ensures the well-formedness of types but is also important to our new rule DS-topVar. An equivalence relation (Definition 3.1) is defined on types that are subtype of each other. These equivalent types can be converted back and forth without loss of information.
that type abstractions of the more specific type (subtype) should have a looser disjointness constraint for the parameter type. ∀X * Top. A denotes that there is no constraint on X , since Top is disjoint to all types. On the contrary, Bot is the strictest constraint. It is useful in types like ∀X * {l : Bot}. A which expresses that X does not contain any informative field of label l [44]. For intersection types, rules DS-andl, DS-andr, and DS-and axiomatize that A & B is the greatest lower bound of A and B. As a typical characteristic of BCD-style subtyping, type constructors distribute over intersections, including arrows (rule DS-distArrow), records (rule DS-distRcd) and disjoint quantifications (rule DS-distAll).
Another feature of BCD subtyping, which is often overlooked, is the generalization of top-like types, i.e. supertypes of Top. The most important change is the rule DS-topVar. This rule means a type variable is top-like if it is disjoint with the bottom type. Every type B is a common supertype of B itself and Bot. If B is disjoint with Bot, then it must be top-like. We proved that subtyping is decidable via an equivalent algorithmic formulation.
The discussion about algorithmic subtyping is in Section 4.1.

Lemma 3.3 (Decidability of subtyping). ∆ A <: B is decidable.
Disjointness. The notion of disjointness (Definition 2.1), defined via subtyping, is used in the original F + i , as well as calculi with disjoint intersection types [30]. We proved that our algorithmic definition of disjointness (written as ∆ A * B, in Section 4.2) is sound to a specification in terms of top-like types.

Lemma 3.4 (Disjointness soundness). If ∆
A * B then ∀C that ∆ A <: C and ∆ B <: C we have ∆ C .
Informally, two disjoint types do not have common supertypes, except for top-like types. This definition is motivated by the desire to prevent ambiguous upcasts on merges. That is, we wish to avoid casts that can extract different values of the same type from a merge. Thus in F + i and other calculi with disjoint intersection types, we only allow merges of expressions whose only common supertypes are types that are (equivalent to) the top type. For instance, consider the merge (1 , , true) , , (

Bidirectional Typing
The type system of F + i is bidirectional [15], where the subsumption rule is triggered by type annotations. Calculi with a merge operator are incompatible with a general subsumption rule because it cancels disjointness checking. For example, with a general subsumption rule, we can directly use 1 , , true as a term of type Int since Int & Bool <: Int. Then, merging 1 , , true with the term false would type-check since disjointness simply checks whether the static types of merging terms are disjoint, and Int is disjoint with Bool. But now, the merge contains two booleans, which would lead to ambiguity if later we wish to extract a boolean value from the merge. The key issue is that a general subsumption rule loses static type information that is necessary to reject ambiguous merges. A bidirectional type system solves this problem by having a more restricted form of subsumption that only works in the checking mode where the type is provided. A more detailed description of the problem for calculi with the merge operator can be found in Huang et al.'s work [22]. We should also remark that this issue of incompatibility with a general subsumption rule is not unique to calculi with a merge operator. It shows up, for instance, in calculi with gradual typing [41] and calculi with record concatenation and subtyping [9].
Typing. As presented in Figure 7, there are two modes of typing: synthesis (⇒) and checking (⇐). We use ⇔ as a metavariable for typing modes. ∆; Γ e ⇔ A indicates that under type context ∆ and term context Γ, the expression e has type A in mode ⇔. A bidirectional type system directly provides a type-checking algorithm. ∆, Γ, e are all inputs in both modes. Type synthesis generates a unique type as the output (also called the inferred type), while type checking takes a type as an input and examines the term. Conversion of typing modes happens in rule Typ-sub. With it, a term with inferred type A can be checked against any B that is a supertype of A. Compared to the original F + i ,  fixpoints are new. They model recursion with a self-reference (x in fix x : A. e). Other than this, rule Typ-fix is almost the same as rule Typ-anno. It checks the expression e by the annotated type A, with assumption that x has type A in e. Application, record projection, and conversion of applicable types. It is not surprising that a merge can act as a function. But in the original F + i , this requires annotations since the expression being applied in an application must have an inferred arrow type. Our design, following the λ + i calculus [22], allows a term of an intersection type to directly apply, as long as the intersection type can be converted into an applicable form. For example, , which is a supertype of the former. When inferring the type of the application e 1 e 2 , rule Typ-app first converts the inferred type of e 1 into an arrow form B → C and then checks the argument e 2 against B. If the check succeeds, the whole expression has inferred type C .
In F + i , we have three applicable forms: arrow types, record types, universal types. Like rule Typ-app, the typing of type application and record projection also allows the applied term to have an intersection type, and relies on applicative distribution to convert the type.
Applicative distribution A B (defined in Figure 8) takes type A and generates a supertype B that has an applicable form. The first three rules bring all parts of the input intersection type together. For example, assuming that we apply several merged functions whose types are It is equivalent to the input type only when A 1 , A 2 , ..., and A n are all equivalent. Essentially, applicative distribution (A B) is a subset of subtyping (A <: B). The supertype is selected to ensure that when a merge is applied to an argument, every component in the merge are satisfied. Although each one of the three first rules overlaps with the reflexivity rule, for any given type, at most one result has an applicable form.
Since merges are treated as a whole applicable term, programmers can extend functions via a compositional approach without modifying the original implementation. It also enables the modular extension of type abstractions and especially records, which play a core role in the trait encoding used in Compositional Programming.
Davies and Pfenning also employ a similar design in their bidirectional type system for refinement intersections [13]. Their type conversion procedure respects subtyping as well. Instead of combining function types, it makes use of A & B <: A and A & B <: B to enumerate components in intersections and uncover arrows.
Typing merges with disjointness and consistency. Well-typed merges always have inferred types. There are two type synthesis rules for merges, both combining the inferred types of the two parts into an intersection. Typ-merge requires the two subterms to have disjoint inferred types, like 1 , , true. Typ-mergev relaxes the disjointness constraint to consistency checking (written as u 1 ≈ u 2 ) to accept overlapping terms like 1 , , 1. Such duplication is meaningless to users but may appear during evaluation. In fact, rule Typ-mergev is designed for metatheory properties, and not to allow more user-written programs [22]. We will state the formal specification of consistency in Section 5.1 and show how it is involved in the proofs of determinism and type soundness. Informally, consistent merges cause no ambiguity in the runtime. For practical reasons, we only consider pre-values (defined at the top of Figure 7) in consistency checking, for which the inferred type can be told directly. The Step Step-fix Step-annov Step-merge e1 → e 1 e2 → e 2 e1 , , e2 → e 1 , , e 2 Step-cntx e → e algorithms for disjointness and consistency are presented in Section 4. In general, disjointness and consistency avoid introducing ambiguity of merges, and enable a deterministic semantics for F + i .

Small-Step Operational Semantics
We specify the call-by-name reduction of F + i using a small-step operational semantics in Figure 9.
Step-papp, Step-pproj, and Step-ptapp are reduction rules for application and record projection. They trigger parallel application (defined in the middle of Figure 9) of merged values to the argument. Rule Step-fix substitutes the fixpoint term variable with the fixpoint expression itself. Note that the result is annotated with A. With the explicit type annotation, the result of reduction preserves the type of the original fixpoint expression. Through rule Step-annov, values are cast to their annotated type. Such values must also be pre-values. This is to filter out checkable terms p including bare abstractions or records without annotations, as p : A is a form of value itself and thus should not step.
A merge of multiple terms may reduce in parallel, as shown in rule Step-merge. Only when one side cannot step, the other side steps alone, as suggested by the evaluation context E , , v and v , , E. Rule Step-cntx is the reduction rule of expressions within an evaluation context. Since the rule can be applied repeatedly, we only need evaluation contexts of depth one (shown at the top of Figure 9). Our operational semantics substitutes arguments wrapped by type annotations into function bodies, while it forbids the reduction of records since records are values.

Parallel application.
Parallel application is at the heart of what we call nested composition in CP. It provides the runtime behavior that is necessary to implement nested composition, and it reflects the subtyping distributivity rules at the term level. A merge of functions is treated as one function. The beta reduction of all functions in a merge happens in parallel to keep the consistency of merged terms. For type abstractions or records, things are similar. The parallel application handles these applicable merges uniformly via rule PApp-merge.
To align record projection with the other two kinds of application, we define arguments which abstract expressions, types, and record labels (at the top of Figure 9). In rule PApp-abs, the argument expression is wrapped by the function argument type before we substitute it into the function body. Parallel application of type abstractions substitutes the type argument into the body and annotates the body with the substituted disjoint quantified type. Rule PApp-proj projects record fields. Note these three rules have types to annotate the result, since in Typ-abs, Typ-tabs, and Typ-rcd we only type the expression e inside in checking mode. With an explicit type annotation, the application preserves types.
Splittable types. Before explaining wrapping or casting, we first introduce splittable types [22], which are a key component of our algorithmic formulations of various relations. Ordinary types are the basic units, values of ordinary types can be constructed without the merge operator. As defined at the top of Figure 10, ordinary types do not have intersection types in positive positions. By contrast, splittable types are isomorphic to appropriate intersections. Recall that in BCD-style distributive rules, arrows distribute over intersection, making Int → Int & Bool equivalent to the intersection (Int → Int) & (Int → Bool). Therefore we say that the former type splits into the latter two arrow types. In Figure 10, we extend the type splitting algorithm of λ + i to universal types in correspondence to the distributive subtyping rules (rule DS-distArrow, rule DS-distRcd, and rule DS-distAll). It gives a decision procedure to check whether a type is splittable or ordinary.

Lemma 3.6 (Type splitting loses no information). B A C only if ·
Expression wrapping. Rules for expression wrapping (e A u) are listed in the middle of Figure 10. Basically, it splits the type A when possible, annotates a duplication of e by each ordinary part of A, and then composes all of them. The only exception is that it never uses top-like types to annotate terms, to avoid ill-typed results like {l = 1} : Int → Top, but rather generates a normal value whose inferred type is that top-like type, like (λx : Int. ) : Int → Top  Figure 10) is the core of the TDOS, and is triggered by the

Casting. Casting (shown in
Step-annov rule. Recalling that only values that are also pre-values will be cast, we can always tell the inferred type of the input value and cast it by any supertype of that inferred type. The definition of casting uses the notion of splittable types. In rule Cast-and, the value is cast under two parts of a splittable type separately, and the results are put together by the merge operator. The following example shows that a merge retains its form when cast under equivalent types. In the latter case, the requested type is a function type, but the result has an intersection type. This change of type causes a major challenge for type preservation. For ordinary types, rule Cast-int casts an integer to itself under type Int. Under any ordinary top-like type, the cast result is the output of the top-like value generator. The casting of values with annotations works by changing the type annotation to the casting (not top-like) supertype. Rule Cast-mergel and rule Cast-merger make a selection between two merged values. The two rules overlap, but for a well-typed value, the casting result is unique.

Sp-and
Example. We show an example to illustrate the behavior of our semantics: Step-annov, Cast-and, and Cast-anno} Step-papp, EW-and, EW-anno, and EW-top} This example shows that a function with a splittable type will be cast to a merge of two copies of itself with different type annotations, i.e., two split results. The application of a merge of functions works by distributing the argument to both functions. Finally, casting selects one side of the merge under the annotated type. From this example, we can see that

Figure 11
Bottom-like type rules and top-like type rules.
without the precise parameter annotation of a lambda function (here Int & Top), there is no way to filter the argument 1 , , true, causing a conflict.

Algorithmics
In Section 3 we have presented several relations in a declarative form, including subtyping, disjointness, and consistency. For the purposes of implementation, it is important to formulate the corresponding algorithmic versions.

Algorithmic Subtyping
To obtain an equivalent algorithmic formulation of subtyping, we firstly define algorithms for top-like types and bottom-like types inductively in Figure 11, then we introduce our algorithmic subtyping and argue that it is equivalent to the declarative subtyping.

Top-like and bottom-like types.
Every top-like type is a supertype of all types (see Definition 3.2), which is equivalent to Top. Compared to the definition of top-like types in the original F + i [7], we add a type context in the subtyping judgment to keep track of type variables that are disjoint to the bottom type. With type contexts, we can derive · ∀X * Bot. X by TL-var since only top-like types are disjoint to Bot. The corresponding declarative subtyping rule is the novel DS-topVar. To eliminate the dependence of our top-like type algorithm on subtyping, we define bottom-like types as a separate relation and use A when ∆ A <: Bot is needed.

Lemma 4.1 (Equivalence of bottom-like types). If ∆ and ∆ A and A if and only if ∆ A <: Bot.
Then we obtain an algorithmic definition of top-like types ( Figure 11) that is equivalent to Definition 3.2.
Algorithmic subtyping. Our subtyping algorithm is shown in Figure 12. This algorithm is an extension of the algorithm used in λ + i with splittable types [22]. The novel additions are the rules involving disjoint polymorphism, which λ + i does not have. While rule S-and requires the supertype B to be splittable, the remaining rules only apply to ordinary B. The basic idea is to split the intersection-like right-hand-side type by rule S-and until types are in more atomic forms, i.e., ordinary, and then apply the remaining rules to decide whether the left-hand-side type is a subtype of each ordinary part. For a subtyping A ≤ B checking to succeed where B is splittable, we need every sub-checking of split types to succeed, as described by the inversion lemma: The key for the distributive subtyping rules to work is encoded in how we split types. For example, only after we split Int → Int & Bool into (Int → Int) and (Int → Bool), it becomes straightforward to tell it is a supertype of (Int → Int) & (Int → Bool). Assuming that we only have rule Sp-and (see Figure 10) that splits intersection types, the system degenerates to the conventional intersection subtyping rules with disjoint polymorphism (like F i ). In other words, the ordinary-type rules (all rules except for rule S-and) are standard and the algorithm design is modular. They are mostly the same as the declarative formulation with the additional ordinary-type condition, except that rules S-andl and S-andr are embedded with transitivity. For two universal types ∀X * A 1 . A 2 and ∀X * B 1 . B 2 , the subtyping of A 1 and B 1 is contravariant, and the subtyping of A 2 and B 2 is covariant. When deciding the subtyping of A 2 and B 2 , we add X * B 1 into the context to track the disjointness of type variable. For the special case of X disjoint to bottom-like types as rule DS-topVar, we have the context to decide X to be top-like by our top-like type algorithm in rule S-top. Our algorithmic subtyping is equivalent to the declarative subtyping and decidable:

Figure 13
Algorithmic type disjointness and pre-value consistency rules.

Disjointness
As shown in Figure 13, the disjointness definition is almost the same as the original F + i [7]. The disjointness judgment ∆ A * B ensures that under the context ∆, any common supertype of A and B is a top-like type. Disjointness helps ensuring the determinism of F + i by forbidding merging terms of types that are not disjoint with each other (rule Typmerge). Basic disjointness axioms A * ax B, such as Int is disjoint with functions, are shown in Appendix A.3. Our algorithm of disjointness is sound with respect to our specification (Lemma 3.4).
Compared to the original F + i , there are two main novelties. Firstly, now the context may tell us if a type variable is top-like, i.e. is disjoint to bottom-like types, and a top-like type variable should be disjoint to any types. Secondly, in rules D-andl and D-andr, we split types instead of allowing only intersection types for the convenience of the proof. We have an alternative disjointness definition in the original style proved to be equivalent in our Coq formalization. We can prove the following properties:

Consistency
Rule Typ-mergev is aimed to type merges of pre-values produced by type casting and expression wrapping. The intention is not to accept more programs, so this rule is not supposed to be exposed to users. The first question is: why are we considering the consistency of pre-values rather than values or expressions? The answer is that our system allows an expression (or a value) to be duplicated, and merged with type annotations in our dynamic semantics by rule Cast-and and rule EW-and. Moreover, it is also allowed to produce a result of duplicated terms with the same type annotation, like 1 : Int , , 1 : Int. Such values cannot pass disjointness checking but are harmless at runtime. To keep type preservation for the application results like the merge after the first and second steps, consistency judgments on annotated terms are necessary. In consistency checking (Figure 13), we take two pre-values and analyze them structurally. A merged pre-value u 1 , , u 2 is consistent to another pre-value u if pre-values composing the merge are consistent with u. Any two basic components from each term must be either disjoint (rule C-disjoint) or only differ in the annotation (except for the argument annotation of lambda abstractions in rule C-anno). For instance, functions with different annotations but the same body are consistent (as the one after the first step in the example above), and 1 , , true is consistent with 1 , , 'a'. Note that we use u : A to represent the principal type of u is A, which is a syntactical approach to compute the types from pre-values. Principal type rules are listed Appendix A.4. Also note that any disjoint pre-values are also consistent. So rule Typ-mergev is a strict relaxation of rule Typ-merge on pre-values.

Type Soundness and Determinism
In this section, we show that the operational semantics of F + i is type-sound and deterministic. In F + i , determinism also plays a key role in the proof of type soundness.

Determinism
A common problem of determinism for calculi with a merge operator is the ambiguity of selection between merged values. In our system, ambiguity is removed by employing disjointness and consistency constraints on merges via typing.
Two values in a merge have no conflicts as long as casting both values under any type leads to the same result. This specification allows v 1 and v 2 to contain identical expressions (may differ in annotations), and terms with disjoint types as such terms can only be cast under top-like types, and the cast result is only decided by that top-like type.

Lemma 5.2 (Top-like casting is term irrelevant). If · A and v
This is because casting only happens when the given type is a supertype of the cast value's type, and disjoint types only share top-like types as common supertypes (Lemma 3.4).

Lemma 5.3 (Upcast only). If ·; · v ⇒ B and v → A v then · B <: A.
With consistency, casting all well-typed values leads to a unique result. The remaining reduction rules, including expression wrapping and parallel application, are trivially deterministic.

Progress
Annotated values trigger casting, for which the progress lemma can be directly proved, as we know v must have an inferred type that is a subtype of B. Lemma 5.6 (Progress of casting). If ·; · v ⇒ A and ·; · v ⇐ B then there exists a v such that v → B v .
The progress lemma for expression wrapping is more relaxed. It does not enforce that e is checked against the wrapping type A because that is the typical situation where we need to use the relation. Parallel applications deal with function application, type application, and record projection. We use the term general application of a value v to an argument arg next to denote all of these for simplicity. Finally, the progress property of reduction can be proved. Theorem 5.9 (Progress of reduction). If ·; · e ⇔ A then either e is a value or there exists a e such that e → e .

Preservation
Retaining preservation is challenging. When typing merges, we need to satisfy the extra side conditions in rules Typ-merge and Typ-mergev: disjointness and consistency. While the former only depends on types, the latter needs special care.
Consistency. As discussed in Section 3.4, casting may duplicate terms. For example, 1 → Int & Int 1 , , 1 by rule Cast-and. Rule Typ-mergev is a relaxation of rule Typ-merge to type such merges. We have to ensure any two merged casting results are consistent: Lemma 5.10 (Value consistency after casting).
Then we need to make sure that consistency is preserved during reduction. Lemma 5.11 (Reduction keeps consistency). If ·; · u 1 ⇒ A and ·; · u 2 ⇒ B and u 1 ≈ u 2 then if u 1 is a value and u 2 → u 2 then u 1 ≈ u 2 ; if u 2 is a value and u 1 → u 1 then u 1 ≈ u 2 ; if u 1 → u 1 and u 2 → u 2 then u 1 ≈ u 2 .
Besides, when parallel application substitutes arguments into merges of applicable terms or projects the wished field, consistency is preserved as well. This requirement enforces us to define consistency not only on values but also on pre-values since the application transforms a value merge into a pre-value merge.
Lemma 5.12 (Parallel application keeps consistency). If ·; · v 1 ⇒ A and ·; · v 2 ⇒ B and v 1 ≈ v 2 and v 1 • arg → u 1 and v 2 • arg → u 2 then u 1 ≈ u 2 when arg is a well-typed expression; or arg is a label; or arg is a type C ; we know A ∀X * A 1 . A 2 and B ∀X * B 1 .
Isomorphic subtyping. In F + i , types are not always precisely preserved by all reduction steps. Specifically, when we cast a value v → A v (in rule Step-annov) or wrap a term e A u (in rule PApp-abs), the context expects v or u to have type A, but this is not always true. In our casting rules shown at the bottom of Figure 10, most values will be reduced to results with the exact type we want, except for rule Cast-and. The inferred type of the result is always an intersection, which may differ from the original splittable type. To describe the change of types during reduction accurately, we define isomorphic subtyping ( Figure 14). If A B, we say A is an isomorphic subtype of B. The following lemma shows that while the two types in an isomorphic subtyping relation may be syntactically different, they are equivalent under an empty type context (i.e. · A <: B and · B <: A).

Theorem 5.13 (Isomorphic subtypes are equivalent). If A B then · A ∼ B.
With isomorphic subtyping, we define the preservation property of casting, expression wrapping, and parallel application as follows.
Lemma 5.14 (Casting preserves typing). If ·; · v ⇒ A and v → B v then there exists a C such that ·; · v ⇒ C and C B. Lemma 5.15 (Expression wrapping preserves typing). If ·; · e ⇐ B and · B <: A and e A u then there exists a C such that ·; · u ⇒ C and C A. Of course, we can prove that the result of casting always has a subtype (or an equivalent type) of the requested type instead of an isomorphic subtype. But it would be insufficient for type preservation of reduction. In summary, if casting or wrapping generates a term of type B when the requested type is A, we need B to satisfy: B is a subtype of A because we want a preservation theorem that respects subtyping.
For any type C , A * C implies B * C . This is for the disjointness and consistency checking in rules Typ-merge and Typ-mergev. Note that B <: A is not enough for this property.
If A converts into an applicable type C , then B converts into an applicable type too.
Although the type equivalence satisfies the first two conditions, it breaks the last one. For example, Top is equivalent to Top → Top, but one may not convert Top to an applicable type by the applicative distribution. So it is infeasible to replace the isomorphic subtyping with the type equivalence.
Narrowing and Substitution Lemmas. Before proving type preservation, we have to prove narrowing and substitution lemmas, including both type and term substitutions. The narrowing lemma for typing is mainly to deal with proof cases regarding universal types. To check an expression against a supertype, we need this property to tighten the disjointness constraint of the type variable in the context of a typing judgment, since a supertype of a universal type has a more tight disjointness constraint. The type substitution lemma for typing is necessary for the instantiation of type variables. We always use types satisfying the disjointness constraint of a universal type to substitute. We need to make sure that the typing judgment still holds after type substitution: In beta reduction or the reduction of fixpoints, we want the term substitution of the parameter inside the function body to always preserve types when the argument has an isomorphic subtype of the function input type. This is different from traditional term substitution lemmas. Our expression wrapping does not necessarily produce a wrapped result with the identical type to the wrapping type (Lemma 5.15). In addition, if we substitute a term with an isomorphic subtype into an expression, the substituted result does not infer the original type: it should infer an isomorphic subtype, though it can still be checked by the original checking type. Finally, with the lemmas above and isomorphic subtyping, we have the type preservation property of F + i . That is, after one or multiple steps of reduction, the inferred type of the reduced expression is an isomorphic subtype. Therefore, for checked expressions, the initial type-checking always succeeds. Theorem 5.21 (Type preservation with isomorphic subtyping). If ·; · e ⇔ A and e → * e then there exists a B such that ·; · e ⇔ B and B A.

Related Work
In the following discussion, sometimes we attach the publication year to its calculus name for easy distinction. For instance, F + i '19 means the original formulation of F + i by Bi et al. [7]. The merge operator, disjoint intersection types and TDOS. The merge operator for calculi with intersection types was proposed by Reynolds [34]. His original formulation came with significant restrictions to ensure that the semantics is not ambiguous. Castagna [11] showed that a merge operator restricted to functions could model overloading. Dunfield [14] proposed a calculus, which we refer to as λ ,, , with an unrestricted merge operator. While powerful, λ ,, lacked both determinism and subject reduction, though type safety was proved via a type-directed elaboration semantics.
To address the ambiguity problems in Dunfield's calculus, Oliveira et al. [30] proposed λ i '16, which only allows intersections of disjoint types. With that restriction and the use of an elaboration semantics, it was then possible to prove the coherence of λ i '16, showing that the semantics was not ambiguous. Bi et al. [6] relaxed the disjointness restriction, requiring it only on merges, in a new calculus called λ + i '18 (or NeColus). This enabled the use of unrestricted intersections in λ + i '18. In addition, they added a more powerful subtyping relation based on the well-known BCD subtyping [4] relation. The new subtyping relation, in turn, enabled nested composition, which is a fundamental feature of Compositional Programming. Unfortunately, both unrestricted intersections and BCD subtyping greatly complicated the coherence proof of λ + i '18. To address those issues, Bi et al. turned to an approach based on logical relations and a notion of contextual equivalence.
To address the increasing complexities arising from the elaboration semantics and the coherence proofs, Huang et al. [20,22] proposed a new approach to model the type-directed semantics of calculi with a merge operator. The type-directed elaboration in λ i '16 and λ + i '18 is replaced by a direct type-directed operational semantics (TDOS). In the new TDOS formulations of λ i and λ + i , coercive subtyping is removed since subtyping no longer needs to generate explicit coercion for the elaboration to a target calculus. Instead, runtime implicit (up)casting is used. This is implemented by the casting relation, which was originally called typed reduction. Our work adopts TDOS and adds disjoint polymorphism. Disjoint polymorphism is used in Compositional Programming to enable techniques such as polymorphic contexts. We also change the evaluation strategy from call-by-value (CBV) to call-by-name (CBN), motivated by the elaboration of trait instantiation in Compositional Programming. Otherwise, with a CBV semantics, many uses of trait instantiation would diverge.
Calculi with disjoint polymorphism. Disjoint polymorphism was originally introduced in a calculus called F i by Alpuim et al. [2]. A disjointness constraint is added to universal quantification in order to allow merging components whose type contains type variables. Later, Bi et al. [7] augment it with distributive subtyping in the F + i '19 calculus. In addition, the bottom type is added and unrestricted intersection types are also allowed to fully encode row and bounded polymorphism [44]. Compared to F + i '19, our new formulation of F + i adopts a direct semantics, based on a TDOS approach, where simpler proofs of determinism supersede the original proofs of coherence. As a result, recursion and impredicative polymorphism can be easily added. Both features are important to fully support the trait encoding in Compositional Programming. A detailed comparison of calculi with a merge operator, which summarizes our discussion on related work, can be found in Figure 15.
There are quite a few typed object encodings in the literature [8], most of which are based on F <: [10]. As it is not our goal in this paper to encode full OOP in F + i , we will not compare our trait encoding with other object encodings. However, it is still  interesting to compare F + i with F <: . Some disadvantages of F <: have been studied in the literature. It has been shown that, with bounded quantification, the subtyping of F <: is undecidable [32], and some useful operations like polymorphic record updates [9] are not directly supported. F + i does not have these drawbacks. F + i has decidable subtyping. For F <: the most common decidable fragment is the so-called kernel F <: variant [10]. Xie et al. [44] have shown that kernel F <: is encodable in F + i . Therefore the bounded quantification that is present in kernel F <: can be expressed in F + i as well. In addition, polymorphic record updates can be easily encoded without extra language constructs. For example, concerning a polymorphic record that contains an x field among others (rcd : { x: Int } & R), the record update { rcd with x = 1 } can be encoded in F + i as { x = 1 } ,, (rcd : R). In other words, we can rewrite whichever fields we want and then merge the remaining polymorphic part back.
F + i versus row-polymorphic calculi. Row polymorphism provides an alternative way to model extensible record types in System F-like calculi. There are many variants of rowpolymorphic calculi in the literature [9,19,24,38]. Among them, the most relevant one with respect to our work is λ || by Harper and Pierce [19]. Disjoint quantification has a striking similarity to constrained quantification in λ || . Their compatibility constraint plays a similar role to disjointness in our system. Furthermore, their merge operator (||) can concatenate either two records like our merge operator ( , , ) or two record types like our intersection type operator ( & ). However, their compatibility constraint and merge operator are only applicable to record types, while we generalize them to arbitrary types. λ || has no subtyping and does not allow for distributivity and nested composition either. Disjoint polymorphism also subsumes the form of row polymorphism present in λ || as demonstrated by Xie et al. [44]. We refer to Xie et al.'s work for an extended discussion of the relationship between F + i and various other row polymorphic calculi.
Semantics for type-dependent languages. The elaboration semantics approach is commonly used to model the semantics of type-dependent languages and calculi. The appeals of the elaboration semantics are simple type-safety proofs, and the fact that they directly offer an implementation technique over conventional languages without a type-dependent semantics. For instance, the semantics of type-dependent languages with type classes [18,43], Scala-style implicits [27,29] or gradual typing [40] all use an elaboration semantics. In contrast, in the past, more conventional direct formulations using an operational semantics have been avoided for languages with a type-dependent semantics. A problem is that the type-dependent semantics introduces complexity in the formulation of an operational semantics, since enough type information should be present at runtime and type information needs to be properly propagated. Early work on the semantics of type classes [23,28], for instance, attempted to employ an operational semantics. However, those approaches had significant practical restrictions in comparison to conventional type classes. The TDOS approach has shown how to overcome important issues when modeling the direct semantics of type-dependent languages. An important advantage of the TDOS approach is that it removes the need for non-trivial coherence proofs. The TDOS approach has also been recently shown to work for modeling the semantics of gradually typed languages directly [45].

Conclusion
In this paper, we presented a new formulation of the F + i calculus and showed how it serves as a direct foundation for Compositional Programming. In contrast to the original F + i , we adopt a direct semantics based on the TDOS approach and embrace call-by-name evaluation. As a result, the metatheory of F + i is significantly simplified, especially due to the fact that a coherence proof based on logical relations and contextual equivalence is not needed. In addition, our formulation of F + i enables recursion and impredicative polymorphism, validating the original trait encoding by Zhang et al. [46]. We proved the type-soundness and determinism of F + i using the Coq proof assistant. Our research explores further possibilities of the TDOS approach and shows some novel notions that could inspire the design of other calculi with similar features.
Although F + i is already expressive enough to work as a core calculus of the CP language, some useful constructs like type operators are missing. We leave the extension of type-level operations for future work. Another interesting design choice that we want to explore is to lazily evaluate both sides of merges, just like what we have done for record fields, which can help avoid some redundant computation on the unused side of a merge. This design choice may be implemented by considering merges of pre-values as values, but the parallel application of pre-value merges needs special care.  Well-formedness relations are defined in Figure 16. ∆ A means type A is well-formed under type context ∆. It checks that all type variables that appear in A are included in ∆.

A.1 Type and Context Well-Formedness
∆ defines well-formed type contexts: any type in the context can only use type variables that are in the context in front of itself. ∆ Γ makes sure types in Γ are all well-formed to ∆.

A.2 Top-like Value Generator
The top-like value generator function is shown as Figure 17, which generates a value inferring the input top-like type.  Principal types (Figure 19), compute the types from pre-values syntatically, using either the annotations available in the pre-values or, for basic values and i, just directly returning the corresponding type. We use u : A to represent the principal type of u is A. This syntactic approach is complete with respect to our type system.

B.2 Type-Checking Subsumption
The type-checking subsumption of our bi-directional type system is restricted within ordinary and not-top-like types, since we may not check arbitrary expressions by all top-like types, such as checking a lambda abstraction against a top-like universal type. Therefore when wrapping an expression by a type annotation, we cannot directly output e : A when A is top-like.