The Essence of Nested Composition

HKU PL Group Papers - Index

Metadata

• Title: The Essence of Nested Composition
• Venue: ECOOP’18
• Area: Merge operator and disjointness
• Source URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.22
• Downloaded PDF: The-Essence-of-Nested-Composition.pdf
• Extracted assets: _assets/The-Essence-of-Nested-Composition/
• Pages: 33
• Embedded image count reported by PyMuPDF: 0

Why this note exists

This note is part of the HKU PL Group literature knowledge base for work on iso-recursive subtyping, intersection types, union types, disjointness, merge operators, and compositional programming. It is designed for later Coding Agent / Proof Agent use during proof search, design brainstorming, and comparison against prior systems.

Extraction quality note

This is the fast pass generated with pymupdf4llm, not the heavier marker-pdf pass. The original PDF is linked above and kept in _pdfs/. Figures/images detected by PyMuPDF are saved under _assets/. Some mathematical notation may still require checking against the PDF, especially inference rules with complex layouts.

Technical landmarks detected automatically

These are line references into the converted Markdown below. They are meant as a quick navigation layer for rules, lemmas, theorems, proofs, algorithms, examples, and counterexamples.

• line 1: The Essence of Nested Composition
• line 3: Xuan Bi[1]
• line 7: Bruno C. d. S. Oliveira[1]
• line 11: Tom Schrijvers[2]
• line 17: Abstract
• line 23: Keywords and phrases nested composition, family polymorphism, intersection types, coherence
• line 31: 1 Introduction
• line 53: 22:2 The Essence of Nested Composition
• line 77: NeColus: a calculus with (disjoint) intersection types that features both BCD-style subtyping and the merge operator . This calculus is both type-safe and coherent, and supports nested composition .
• line 95: 2 Overview
• line 99: 2.1 Motivation: Family Polymorphism
• line 127: 2.2 The Expression Problem, NeColus Style
• line 135: 22:6 The Essence of Nested Composition
• line 141: Similarly, we capture the interface of the Lang family in a record, with one field for each case’s constructor.
• line 157: We obtain an implementation for LangEval by merging the existing Lang implementation implLang with the new evaluation functionality implEval using the merge operator ,, .
• line 189: Similarly, the multi-field record expression in the definition of implLang is syntactic sugar for the explicit merge of two single-field records.
• line 227: 2.3 Disjoint Intersection Types and Ambiguity
• line 239: types have to be disjoint, i.e., Nat & Nat is ill-formed because the first component has the same type as the second.
• line 243: 2.4 Logical Relations for Coherence
• line 251: 3 NeColus: Syntax and Semantics
• line 264: |Typing contexts|Γ|::=|• |Γ, x :A|
• line 268: Figure 3 Syntax of NeColus.
• line 278: Figure 4 Declarative specification of subtyping.
• line 280: 3.1 Syntax
• line 284: 3.2 Declarative Subtyping
• line 286: Figure 4 presents the subtyping relation. We ignore the highlighted parts, and explain them later in Section 3.4.
• line 314: 3.3 Typing of NeColus
• line 326: 22:12 The Essence of Nested Composition
• line 333: Figure 6 Disjointness.
• line 337: |Typing contexts|∆|::=|• |∆, x :τ|
• line 349: 3.4 Elaboration Semantics
• line 363: (Coercion typing)
• line 367: Figure 8 Coercion typing.
• line 371: Target Typing. The typing of λc has the form ∆ ⊢ e : τ , which is entirely standard. Only the typing of coercion applications, shown below, deserves attention:
• line 377: Here the judgement c ⊢ τ 1 ▷τ 2 expresses the typing of coercions, which are essentially functions from τ 1 to τ 2. Their typing rules correspond exactly to the subtyping rules of NeColus, as shown in Fig. 8.
• line 381: - Theorem 1 (Preservation) . If • ⊢ e : τ and e −→ e[′] , then • ⊢ e[′] : τ .
• line 383: - Theorem 2 (Progress) . If • ⊢ e : τ , then either e is a value, or ∃e[′] such that e −→ e[′] .
• line 387: To conclude, we show two lemmas that relate NeColus expressions to λc terms.
• line 389: - Lemma 3 (Coercions preserve types) . If A < : B ⇝ c, then c ⊢|A| ▷ |B|.
• line 395: 22:14 The Essence of Nested Composition
• line 407: Proof. By structural induction on the derivation of subtyping.
• line 411: ▶ Lemma 4 (Elaboration soundness) . We have that: If Γ ⊢ E ⇒ A ⇝ e, then | Γ | ⊢ e : |A|. If Γ ⊢ E ⇐ A ⇝ e, then | Γ | ⊢ e : |A|.
• line 413: Proof. By structural induction on the derivation of typing. ◀
• line 415: 3.5 Comparison with λi
• line 429: X. Bi, B. C. d. S. Oliveira, and T. Schrijvers
• line 433: 4 Coherence
• line 437: 4.1 In Search of Coherence
• line 465: Regarding Example 5, it seems adequate to say that 3 and id 3 are contextually equivalent. Does this imply that coherence can be based on Definition 7? Unfortunately it cannot, as demonstrated by the following example.
• line 513: For the same reason as in Definition 9, we only consider expressions in the inference mode. The rest of the section is devoted to proving that Theorem 10 holds.
• line 515: 4.2 Logical Relations
• line 549: ▶ Lemma 11 (Disjoint values are in a value relation) . If A 1 ∗ A 2 and v 1 : |A 1 | and v 2 : |A 2 |, then ( v 1 , v 2) ∈V � |A 1 | ; |A 2 | � .
• line 551: Proof. By induction on the derivation of disjointness.
• line 557: Logical Equivalence. The logical relations can be lifted to open terms in the usual way. First we give the semantic interpretation of typing contexts:
• line 559: ▶ Definition 12 (Interpretation of Typing Contexts) . ( γ 1 , γ 2) ∈G �∆1; ∆2� is defined as follows:
• line 581: 4.3 Establishing Coherence
• line 583: With all the machinery in place, we are now ready to prove Theorem 10. But we need several lemmas to set the stage.
• line 589: Proof. By induction on the typing derivation of the coercion c . ◀
• line 593: - Theorem 15 (Inference Uniqueness) . If Γ ⊢ E ⇒ A 1 and Γ ⊢ E ⇒ A 2 , then A 1 ≡ A 2 .
• line 595: - Theorem 16 (Fundamental Property) . We have that: If Γ ⊢ E ⇒ A ⇝ e and Γ ⊢ E ⇒ A ⇝ e[′] , then | Γ | ⊢ e ⋍ log e[′] : |A|. If Γ ⊢ E ⇐ A ⇝ e and Γ ⊢ E ⇐ A ⇝ e[′] , then | Γ | ⊢ e ⋍ log e[′] : |A|.
• line 603: ▶ Lemma 17 (Congruence) . If C : (Γ ⇔ A ) �→ (Γ [′] ⇔[′] A[′] ) ⇝ D, Γ ⊢ E 1 ⇔ A ⇝ e 1 , Γ ⊢ E 2 ⇔ A ⇝ e 2 and | Γ | ⊢ e 1 ⋍ log e 2 : |A|, then | Γ [′] | ⊢De 1 ⋍ log De 2 : |A[′] |.
• line 605: Proof. By induction on the typing derivation of the context C , and applying the compatibility lemmas where appropriate. ◀
• line 607: - Lemma 18 (Adequacy) . If • ⊢ e 1 ⋍ log e 2 : Nat then e 1 ⋍ e 2 .
• line 609: Proof. Adequacy follows easily from the definition of the logical relation. ◀
• line 611: Next up is the proof that logical relation is sound with respect to contextual equivalence:
• line 613: ▶ Theorem 19 (Soundness w.r.t. Contextual Equivalence) . If Γ ⊢ E 1 ⇒ A ⇝ e 1 and Γ ⊢ E 2 ⇒ A ⇝ e 2 and | Γ | ⊢ e 1 ⋍ log e 2 : |A| then Γ ⊢ E 1 ⋍ ctx E 2 : A.
• line 615: Proof. From Definition 9, we are given a context C : (Γ ⇒ A ) �→ ( • ⇒ Nat) ⇝ D . By Lemma 17 we have • ⊢De 1 ⋍ log De 2 : Nat, thus De 1 ⋍ De 2 by Lemma 18. ◀
• line 623: Armed with Theorem 16 and Theorem 19, coherence follows directly.
• line 625: ▶ Theorem 10 (Coherence) . If Γ ⊢ E ⇒ A then Γ ⊢ E ⋍ ctx E : A.
• line 627: Proof. Immediate from Theorem 16 and Theorem 19.
• line 631: 4.4 Some Interesting Corollaries
• line 633: To showcase the strength of the new proof method, we can derive some interesting corollaries. For the most part, they are direct consequences of logical equivalence which carry over to contextual equivalence.
• line 637: ▶ Corollary 20 (Merge is Neutral) . If Γ ⊢ E 1 ⇒ A and Γ ⊢ E 1 , , E 2 ⇒ A, then Γ ⊢ E 1 ⋍ ctx E 1 , , E 2 : A
• line 639: ▶ Corollary 21 (Merge is Commutative) . If Γ ⊢ E 1 , , E 2 ⇒ A and Γ ⊢ E 2 , , E 1 ⇒ A, then Γ ⊢ E 1 , , E 2 ⋍ ctx E 2 , , E 1 : A.
• line 641: ▶ Corollary 22 (Merge is Associative) . If Γ ⊢ ( E 1 , , E 2) , , E 3 ⇒ A and Γ ⊢ E 1 , , ( E 2 , , E 3) ⇒ A, then Γ ⊢ ( E 1 , , E 2) , , E 3 ⋍ ctx E 1 , , ( E 2 , , E 3) : A.
• line 643: ▶ Corollary 23 (Coercions Preserve Semantics) . If A < : B ⇝ c 1 and A < : B ⇝ c 2 , then ∆ ⊢ λx. c 1 x ⋍ log λx. c 2 x : |A| →|B|.
• line 645: 5 Algorithmic Subtyping
• line 649: 5.1 The Subtyping Algorithm
• line 667: Figure 12 Algorithmic subtyping of NeColus.
• line 697: 5.2 Correctness of the Algorithm
• line 701: Soundness of the Algorithm. The proof of soundness is straightforward.

Full converted paper text

The Essence of Nested Composition

Xuan Bi[1]

The University of Hong Kong, Hong Kong, China xbi@cs.hku.hk

Bruno C. d. S. Oliveira[1]

The University of Hong Kong, Hong Kong, China bruno@cs.hku.hk

Tom Schrijvers[2]

KU Leuven, Belgium

tom.schrijvers@cs.kuleuven.be

Abstract

Calculi with disjoint intersection types support an introduction form for intersections called the merge operator , while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition , which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce’s work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations . Our work has been fully formalized in Coq, and we have an implementation of our calculus.

2012 ACM Subject Classification Software and its engineering → Object oriented languages

Keywords and phrases nested composition, family polymorphism, intersection types, coherence

Digital Object Identifier 10.4230/LIPIcs.ECOOP.2018.22

Supplement Material ECOOP Artifact Evaluation approved artifact available at http://dx.doi.org/10.4230/DARTS.4.3.5

Acknowledgements We thank the anonymous reviewers for their helpful comments.

1 Introduction

Intersection types [49, 18] have a long history in programming languages. They were originally introduced to characterize exactly all strongly normalizing lambda terms. Since then, starting with Reynolds’s work on Forsythe [54], they have also been employed to express

1 Funded by Hong Kong Research Grant Council projects number 17210617 and 17258816

2 Funded by The Research Foundation - Flanders

© Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers; licensed under Creative Commons License CC-BY

----- Start of picture text -----
o
Cfam
i
p
OOCPE* ACoenssiusetrentt clettemWueclolD * E AEC
* R nev
dot eta
l
d
e
y
u
s *
t
a
a
E
----- End of picture text -----

32nd European Conference on Object-Oriented Programming (ECOOP 2018). Editor: Todd Millstein; Article No. 22; pp. 22:1–22:33 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

--- end of page.page_number=1 ---

22:2 The Essence of Nested Composition

useful programming language constructs, such as key aspects of multiple inheritance [17] in Object-Oriented Programming (OOP). One notable example is the Scala language [44] and its DOT calculus [3], which make fundamental use of intersection types to express a class/trait that extends multiple other traits. Other modern languages, such as TypeScript [39], Flow [28] and Ceylon [51], also adopt some form of intersection types.

Intersection types come in different varieties in the literature. Some calculi provide an explicit introduction form for intersections, called the merge operator . This operator was introduced by Reynolds in Forsythe [54] and adopted by a few other calculi [15, 23, 46, 2]. Unfortunately, while the merge operator is powerful, it also makes it hard to get a coherent (or unambiguous) semantics. Unrestricted uses of the merge operator can be ambiguous, leading to an incoherent semantics where the same program can evaluate to different values. A far more common form of intersection types are the so-called refinement types [30, 21, 24]. Refinement types restrict the formation of intersection types so that the two types in an intersection are refinements of the same simple (unrefined) type. Refinement intersection increases only the expressiveness of types and not of terms. For this reason, Dunfield [23] argues that refinement intersection is unsuited for encoding various useful language features that require the merge operator (or an equivalent term-level operator).

Disjoint Intersection Types. λi is a recent calculus with a variant of intersection types called disjoint intersection types [46]. Calculi with disjoint intersection types feature the merge operator, with restrictions that all expressions in a merge operator must have disjoint types and all well-formed intersections are also disjoint. A bidirectional type system and the disjointness restrictions ensure that the semantics of the resulting calculi remains coherent. Disjoint intersection types have great potential to serve as a foundation for powerful, flexible and yet type-safe OO languages that are easy to reason about. As shown by Alpuim et al. [2], calculi with disjoint intersection types are very expressive and can be used to statically type-check JavaScript-style programs using mixins. Yet they retain both type safety and coherence. While coherence may seem at first of mostly theoretical relevance, it turns out to be very relevant for OOP. Multiple inheritance is renowned for being tricky to get right, largely because of the possible ambiguity issues caused by the same field/method names inherited from different parents [9, 58]. Disjoint intersection types enforce that the types of parents are disjoint and thus that no conflicts exist. Any violations are statically detected and can be manually resolved by the programmer. This is very similar to existing trait models [29, 22]. Therefore in an OO language modelled on top of disjoint intersection types, coherence implies that no ambiguity arises from multiple inheritance. This makes reasoning a lot simpler.

Family Polymorphism. One powerful and long-standing idea in OOP is family polymorphism [25]. In family polymorphism inheritance is extended to work on a whole family of classes , rather than just a single class. This enables high degrees of modularity and reuse, including simple solutions to hard programming language problems, like the Expression Problem [64]. An essential feature of family polymorphism is nested composition [19, 27, 42], which allows the automatic inheritance/composition of nested (or inner) classes when the top-level classes containing them are composed. Designing a sound type system that fully supports family polymorphism and nested composition is notoriously hard; there are only a few, quite sophisticated, languages that manage this [27, 42, 16, 57].

--- end of page.page_number=2 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:3

NeColus. This paper presents an improved variant of λi called NeColus[3] (or λ[+] i[):][a][simple] calculus with records and disjoint intersection types that supports nested composition . Nested composition enables encoding simple forms of family polymorphism. More complex forms of family polymorphism, involving binary methods [11] and mutable state are not yet supported, but are interesting avenues for future work. Nevertheless, in NeColus, it is possible, for example, to encode Ernst’s elegant family-polymorphism solution [25] to the Expression Problem. Compared to λi the essential novelty of NeColus are distributivity rules between function/record types and intersection types. These rules are the delta that enable extending the simple forms of multiple inheritance/composition supported by λi into a more powerful form supporting nested composition. The distributivity rule between function types and intersections is common in calculi with intersection types aimed at capturing the set of all strongly normalizable terms, and was first proposed by Barendregt et al. [4] (BCD). However the distributivity rule is not common in calculi or languages with intersection types aimed at programming. For example the rules employed in languages that support intersection types (such as Scala, TypeScript, Flow or Ceylon) lack distributivity rules. Moreover distributivity is also missing from several calculi with a merge operator. This includes all calculi with disjoint intersection types and Dunfield’s work on elaborating intersection types, which was the original foundation for λi . A possible reason for this omission in the past is that distributivity adds substantial complexity (both algorithmically and metatheoretically), without having any obvious practical applications. This paper shows how to deal with the complications of BCD subtyping, while identifying a major reason to include it in a programming language: BCD enables nested composition and subtyping, which is of significant practical interest.

NeColus differs significantly from previous BCD-based calculi in that it has to deal with the possibility of incoherence, introduced by the merge operator. Incoherence is a non-issue in the previous BCD-based calculi because they do not feature this merge operator or any other source of incoherence. Although previous work on disjoint intersection types proposes a solution to coherence, the solution imposes several ad-hoc restrictions to guarantee the uniqueness of the elaboration and thus allow for a simple syntactic proof of coherence. Most importantly, it makes it hard or impossible to adapt the proof to extensions of the calculus, such as the new subtyping rules required by the BCD system.

In this work we remove the brittleness of the previous syntactic method to prove coherence, by employing a more semantic proof method based on logical relations [63, 48, 61]. This new proof method has several advantages. Firstly, with the new proof method, several restrictions that were enforced by λi to enable the syntactic proof method are removed. For example the work on λi has to carefully distinguish between so-called top-like types and other types. In NeColus this distinction is not necessary; top-like types are handled like all other types. Secondly, the method based on logical relations is more powerful because it is based on semantic rather than syntactic equality. Finally, the removal of the ad-hoc side-conditions makes adding new extensions, such as support for BCD-style subtyping, easier. In order to deal with the complexity of the elaboration semantics of NeColus, we employ binary logical relations that are heterogeneous, parameterized by two types; the fundamental property is also reformulated to account for bidirectional type-checking.

In summary the contributions of this paper are:

NeColus: a calculus with (disjoint) intersection types that features both BCD-style subtyping and the merge operator . This calculus is both type-safe and coherent, and supports nested composition .

3 NeColus stands for Ne sted Co mposition calcu lus .

ECOOP 2018

--- end of page.page_number=3 ---

22:4 The Essence of Nested Composition

• A more flexible notion of disjoint intersection types where only merges need to be checked for disjointness. This removes the need for enforcing disjointness for all well-formed types, making the calculus more easily extensible.

• An extension of BCD subtyping with both records and elaboration into coercions, and algorithmic subtyping rules with coercions, inspired by Pierce’s decision procedure [47]. A more powerful proof strategy for coherence of disjoint intersection types based on logical relations.

• Illustrations of how the calculus can encode essential features of family polymorphism through nested composition.

• A comprehensive Coq mechanization of all meta-theory. This has notably revealed several missing lemmas and oversights in Pierce’s manual proof [47] of BCD’s algorithmic subtyping. We also have an implementation of a language built on top of NeColus; it runs and type-checks all examples shown in the paper.[4]

2 Overview

This section illustrates NeColus with an encoding of a family polymorphism solution to the Expression Problem, and informally presents its salient features.

2.1 Motivation: Family Polymorphism

In OOP family polymorphism is the ability to simultaneously refine a family of related classes through inheritance. This is motivated by a need to not only refine individual classes, but also to preserve and refine their mutual relationships. Nystrom et al. [42] call this scalable extensibility : “the ability to extend a body of code while writing new code proportional to the differences in functionality”. A well-studied mechanism to achieve family inheritance is nested inheritance [42]. Nested inheritance combines two aspects. Firstly, a class can have nested class members; the outer class is then a family of (inner) classes. Secondly, when one family extends another, it inherits (and can override) all the class members, as well as the relationships within the family (including subtyping) between the class members. However, the members of the new family do not become subtypes of those in the parent family.

The Expression Problem, Scandinavian Style. Ernst [25] illustrates the benefits of nested inheritance for modularity and extensibility with one of the most elegant and concise solutions to the Expression Problem [64]. The objective of the Expression Problem is to extend a datatype, consisting of several cases, together with several associated operations in two dimensions: by adding more cases to the datatype and by adding new operations for the datatype. Ernst solves the Expression Problem in the gbeta language, which he adorns with a Java-like syntax for presentation purposes, for a small abstract syntax tree (AST) example. His starting point is the code shown in Fig. 1a. The outer class Lang contains a family of related AST classes: the common superclass Exp and two cases, Lit for literals and Add for addition. The AST comes equipped with one operation, toString , which is implemented by both cases.

4 The Coq formalization and implementation are available at https://goo.gl/R5hUAp .

--- end of page.page_number=4 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:5

class Lang { // Adding a new operation virtual class Exp { class LangEval extends Lang { String toString() {} refine class Exp { } int eval() {} virtual class Lit extends Exp { } int value; refine class Lit { Lit( int value) { int eval { return value; } this .value = value; } } refine class Add { String toString() { int eval { return return value; left.eval() + right.eval(); } } } } virtual class Add extends Exp { } Exp left,right; // Adding a new case Add(Exp left, Exp right) { class LangNeg extends Lang { this .left = left; virtual class Neg extends Exp { this .right = right; Neg(Exp exp) { this .exp = exp; } } String toString() { String toString() { return "-(" + exp + ")"; return left + "+" + right; } } Exp exp; } } } }

• (a) Base family: the language Lang . (b) Extending in two dimensions.

Figure 1 The Expression Problem, Scandinavian Style.

Adding a New Operation. One way to extend the family is to add an additional evaluation operation, as shown in the top half of Fig. 1b. This is done by subclassing the Lang class and refining all the contained classes by implementing the additional eval method. Note that the inheritance between, e.g., Lang.Exp and Lang.Lit is transferred to LangEval.Exp and LangEval.Lit . Similarly, the Lang.Exp type of the left and right fields in Lang.Add is automatically refined to LangEval.Exp in LangEval.Add .

Adding a New Case. A second dimension to extend the family is to add a case for negation, shown in the bottom half of Fig. 1b. This is similarly achieved by subclassing Lang , and now adding a new contained class Neg , for negation, that implements the toString operation. Finally, the two extensions are naturally combined by means of multiple inheritance, closing the diamond.

class LangNegEval extends LangEval & LangNeg { refine class Neg { int eval() { return -exp.eval(); } } }

The only effort required is to implement the one missing operation case, evaluation of negated expressions.

2.2 The Expression Problem, NeColus Style

The NeColus calculus allows us to solve the Expression Problem in a way that is very similar to Ernst’s gbeta solution. However, the underlying mechanisms of NeColus are quite different

ECOOP 2018

--- end of page.page_number=5 ---

22:6 The Essence of Nested Composition

from those of gbeta. In particular, NeColus features a structural type system in which we can model objects with records, and object types with record types. For instance, we model the interface of Lang.Exp with the singleton record type { print : String } . For the sake of conciseness, we use type aliases to abbreviate types.

type IPrint = { print : String };

Similarly, we capture the interface of the Lang family in a record, with one field for each case’s constructor.

type Lang = { lit : Int → IPrint, add : IPrint → IPrint → IPrint };

Here is the implementation of Lang .

implLang : Lang = { lit (value : Int ) = { print = value.toString }, add (left : IPrint) (right : IPrint) = { print = left.print ++ "+" ++ right.print } };

Adding Evaluation. We obtain IPrint & IEval , which is the corresponding type for LangEval.Exp , by intersecting IPrint with IEval where

type IEval = { eval : Int };

The type for LangEval is then:

type LangEval = { lit : Int → IPrint & IEval, add : IPrint & IEval → IPrint & IEval → IPrint & IEval };

We obtain an implementation for LangEval by merging the existing Lang implementation implLang with the new evaluation functionality implEval using the merge operator ,, .

implEval = { lit (value : Int ) = { eval = value }, add (left : IEval) (right : IEval) = { eval = left.eval + right.eval } }; implLangEval : LangEval = implLang ,, implEval;

Adding Negation. Adding negation to Lang works similarly.

type NegPrint = { neg : IPrint → IPrint }; type LangNeg = Lang & NegPrint; implNegPrint : NegPrint = { neg (exp : IPrint) = { print = "-" ++ exp.print } }; implLangNeg : LangNeg = implLang ,, implNegPrint;

--- end of page.page_number=6 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:7

Putting Everything Together. Finally, we can combine the two extensions and provide the missing implementation of evaluation for the negation case.

type NegEval = { neg : IEval → IEval}; implNegEval : NegEval = { neg (exp : IEval) = { eval = 0 - exp.eval } };

type NegEvalExt = { neg : IPrint & IEval → IPrint & IEval }; type LangNegEval = LangEval & NegEvalExt; implLangNegEval : LangNegEval = implLangEval ,, implNegPrint ,, implNegEval;

We can test implLangNegEval by creating an object e of expression − 2 + 3 that is able to print and evaluate at the same time.

fac=implLangNegEval;
e=fac.add(fac.neg(fac.lit2))(fac.lit3);
main=e.print++"="++e.eval.toString--Output:"-2+3=1"

Multi-Field Records. One relevant remark is that NeColus does not have multi-field record types built in. They are merely syntactic sugar for intersections of single-field record types. Hence, the following is an equivalent definition of Lang :

type Lang = {lit : Int → IPrint} & {add : IPrint → IPrint → IPrint};

Similarly, the multi-field record expression in the definition of implLang is syntactic sugar for the explicit merge of two single-field records.

implLang:Lang={lit=...},,{add=...};

Subtyping. A big difference compared to gbeta is that many more NeColus types are related through subtyping. Indeed, gbeta is unnecessarily conservative [26]: none of the families is related through subtyping, nor is any of the class members of one family related to any of the class members in another family. For instance, LangEval is not a subtype of Lang , nor is LangNeg.Lit a subtype of Lang.Lit .

In contrast, subtyping in NeColus is much more nuanced and depends entirely on the structure of types. The primary source of subtyping are intersection types: any intersection type is a subtype of its components. For instance, IPrint & IEval is a subtype of both IPrint and IEval . Similarly LangNeg = Lang & NegPrint is a subtype of Lang . Compare this to gbeta where LangEval.Expr is not a subtype of Lang.Expr , nor is the family LangNeg a subtype of the family Lang .

However, gbeta and NeColus agree that LangEval is not a subtype of Lang . The NeColusside of this may seem contradictory at first, as we have seen that intersection types arise from the use of the merge operator, and we have created an implementation for LangEval with implLang ,, implEval where implLang : Lang . That suggests that LangEval is a subtype of Lang . Yet, there is a flaw in our reasoning: strictly speaking, implLang ,, implEval is not of type LangEval but instead of type Lang & EvalExt , where EvalExt is the type of implEval :

type EvalExt = { lit : Int → IEval, add : IEval → IEval → IEval };

Nevertheless, the definition of implLangEval is valid because Lang & EvalExt is a subtype of LangEval . Indeed, if we consider for the sake of simplicity only the lit field, we have that ( Int → IPrint) & ( Int → IEval) is a subtype of Int → IPrint & IEval . This follows from

ECOOP 2018

--- end of page.page_number=7 ---

22:8 The Essence of Nested Composition

----- Start of picture text -----
NegEvalExt LangEval
LangNegEval
NegEval NegPrint Lang EvalExt
NegEval & NegPrint LangNeg Lang & EvalExt
implNegEval
,,
implNegEval implNegPrint implNegPrint implLangNeg implLang implLangEval implEval
implLangNegEval
LEGEND:
# Interface # implmentation subtype-of impl-of
# composition
----- End of picture text -----

Figure 2 Summary diagram of the relationships between language components.

a standard subtyping axiom for distributivity of functions and intersections in the BCD system inherited by NeColus. In conclusion, Lang & EvalExt is a subtype of both Lang and of LangEval . However, neither of the latter two types is a subtype of the other. Indeed, LangEval is not a subtype of Lang as the type of add is not covariantly refined and thus admitting the subtyping is unsound. For the same reason Lang is not a subtype of LangEval .

Figure 2 shows the various relationships between the language components. Admittedly, the figure looks quite complex because our calculus features a structural type system (as often more foundational calculi do), whereas mainstream OO languages have nominal type systems. This is part of the reason why we have so many subtyping relations in Fig. 2.

Stand-Alone Extensions. Unlike in gbeta and other class-based inheritance systems, in NeColus the extension implEval is not tied to LangEval . In that sense, it resembles trait and mixin systems that can apply the same extension to different classes. However, unlike those systems, implEval can also exist as a value on its own, i.e., it is not an extension per se.

2.3 Disjoint Intersection Types and Ambiguity

The above example shows that intersection types and the merge operator are closely related to multiple inheritance. Indeed, they share a major concern with multiple inheritance, namely ambiguity. When a subclass inherits an implementation of the same method from two different parent classes, it is unclear which of the two methods is to be adopted by the subclass. In the case where the two parent classes have a common superclass, this is known as the diamond problem . The ambiguity problem also appears in NeColus, e.g., if we merge two numbers to obtain 1 , , 2 of type Nat & Nat. Is the result of 1 , , 2 + 3 either 4 or 5?

Disjoint intersection types offer to statically detect potential ambiguity and to ask the programmer to explicitly resolve the ambiguity by rejecting the program in its ambiguous form. In the previous work on λi , ambiguity is avoided by dictating that all intersection

--- end of page.page_number=8 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:9

types have to be disjoint, i.e., Nat & Nat is ill-formed because the first component has the same type as the second.

Duplication is Harmless. While requiring that all intersections are disjoint is sufficient to guarantee coherence, it is not necessary. In fact, such requirement unnecessarily encumbers the subtyping definition with disjointness constraints and an ad-hoc treatment of “top-like” types. Indeed, the value 1 , , 1 of the non-disjoint type Nat & Nat is entirely unambiguous, and (1 , , 1) + 3 can obviously only result in 4. More generally, when the overlapping components of an intersection type have the same value, there is no ambiguity problem. NeColus uses this idea to relax λi ’s enforcement of disjointness. In the case of a merge, it is hard to statically decide whether the two arguments have the same value, and thus NeColus still requires disjointness. This is why in Fig. 2 we cannot define implLangNegEval by directly composing the two existing implLangEval and implLangNeg , even though the latter two both contain the same implLang . Yet, disjointness is no longer required for the well-formedness of types and overlapping intersections can be created implicitly through subtyping, which results in duplicating values at runtime. For instance, while 1 , , 1 is not expressible 1 : Nat & Nat creates the equivalent value implicitly. In short, duplication is harmless and subtyping only generates duplicated values for non-disjoint types.

2.4 Logical Relations for Coherence

Coherence is easy to establish for λi as its rigid rules mean that there is at most one possible subtyping derivation between any two types. As a consequence there is only one possible elaboration and thus one possible behavior for any program.

Two factors make establishing coherence for NeColus much more difficult: the relaxation of disjointness and the adoption of the more expressive subtyping rules from the BCD system (for which λi lacks). These two factors mean that subtyping proofs are no longer unique and hence that there are multiple elaborations of the same source program. For instance, Nat & Nat is a subtype of Nat in two ways: by projection on either the first or second component. Hence the fact that all elaborations yield the same result when evaluated has become a much more subtle property that requires sophisticated reasoning. For instance, in the example, we can see that coherence holds because at runtime any value of type Nat & Nat has identical components, and thus both projections yield the same result.

For NeColus in general, we show coherence by capturing the non-ambiguity invariant in a logical relation and showing that it is preserved by the operational semantics. A complicating factor is that not one, but two languages are involved: the source language NeColus and the target language, essentially the simply-typed lambda calculus extended with coercions and records. The logical relation does not hold for target programs and program contexts in general, but only for those that are the image of a corresponding source program or program context. Thus we must view everything through the lens of elaboration.

3 NeColus: Syntax and Semantics

In this section we formally present the syntax and semantics of NeColus. Compared to prior work [2, 46], NeColus has a more powerful subtyping relation. The new subtyping relation is inspired by BCD-style subtyping, but with two noteworthy differences: subtyping is coercive (in contrast to traditional formulations of BCD); and it is extended with records. We also have a new target language with explicit coercions inspired by the coercion calculus of Henglein [32]. A full technical comparison between λ[+] i[and] [λ][i][can][be][found][in][Section][3.5.]

ECOOP 2018

--- end of page.page_number=9 ---

22:10 The Essence of Nested Composition

|Types|A, B, C|::=|Nat_| ⊤| A →B | A_&B | {l :A}| |---|---|---|---| |Expressions|E|::=|x | i | ⊤| λx. E | E_1_E_2 | E_1, , E_2 | E :A | {l =E} | E.l| |Typing contexts|Γ|::=|• |Γ, x_ :A|

Figure 3 Syntax of NeColus.

----- Start of picture text -----
A < : B ⇝ c (Declarative subtyping)
S-trans
S-refl S-top
A 2 < : A 3 ⇝ c 1 A 1 < : A 2 ⇝ c 2
A < : A ⇝ id A 1 < : A 3 ⇝ c 1 ◦ c 2 A < : ⊤ ⇝ top
S-rcd S-arr
A < : B ⇝ c B 1 < : A 1 ⇝ c 1 A 2 < : B 2 ⇝ c 2 S-andl
{l : A} < : {l : B} ⇝ {l : c} A 1 → A 2 < : B 1 → B 2 ⇝ c 1 → c 2 A 1 & A 2 < : A 1 ⇝ π 1
S-and
S-andr A 1 < : A 2 ⇝ c 1 A 1 < : A 3 ⇝ c 2
A 1 & A 2 < : A 2 ⇝ π 2 A 1 < : A 2 & A 3 ⇝ ⟨c 1 , c 2 ⟩
S-distArr S-topArr
( A 1 → A 2) & ( A 1 → A 3) < : A 1 → A 2 & A 3 ⇝ dist → ⊤ < : ⊤→⊤ ⇝ top →
S-distRcd S-topRcd
{l : A} & {l : B} < : {l : A & B} ⇝ dist {l} ⊤ < : {l : ⊤} ⇝ top {l}
----- End of picture text -----

Figure 4 Declarative specification of subtyping.

3.1 Syntax

Figure 3 shows the syntax of NeColus. For brevity of the meta-theoretic study, we do not consider primitive operations on natural numbers, or other primitive types. They can be easily added to the language, and our prototype implementation is indeed equipped with common primitive types and their operations. Metavariables A, B, C range over types. Types include naturals Nat, a top type ⊤ , function types A → B , intersection types A & B , and singleton record types {l : A} . Metavariable E ranges over expressions. Expressions include variables x , natural numbers i , a canonical top value ⊤ , lambda abstractions λx. E , applications E 1 E 2, merges E 1 , , E 2, annotated terms E : A , singleton records {l = E} , and record selections E.l .

3.2 Declarative Subtyping

Figure 4 presents the subtyping relation. We ignore the highlighted parts, and explain them later in Section 3.4.

BCD-Style Subtyping. The subtyping rules are essentially those of the BCD type system [4], extended with subtyping for singleton records. Rules S-top and S-rcd for top types and record types are straightforward. Rule S-arr for function subtyping is standard. Rules S- andl, S-andr, and S-and for intersection types axiomatize that A & B is the greatest lower bound of A and B . Rule S-distArr is perhaps the most interesting rule. This, so-called “distributivity” rule, describes the interaction between the subtyping relations for

--- end of page.page_number=10 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:11

----- Start of picture text -----
Γ ⊢ E ⇒ A ⇝ e (Inference)
T-app
T-top T-lit T-var Γ ⊢ E 1 ⇒ A 1 → A 2 ⇝ e 1
x : A ∈ Γ Γ ⊢ E 2 ⇐ A 1 ⇝ e 2
Γ ⊢⊤⇒⊤ ⇝ ⟨⟩ Γ ⊢ i ⇒ Nat ⇝ i Γ ⊢ x ⇒ A ⇝ x Γ ⊢ E 1 E 2 ⇒ A 2 ⇝ e 1 e 2
T-merge
T-anno T-proj Γ ⊢ E 1 ⇒ A 1 ⇝ e 1
Γ ⊢ E ⇐ A ⇝ e Γ ⊢ E ⇒{l : A} ⇝ e Γ ⊢ E 2 ⇒ A 2 ⇝ e 2 A 1 ∗ A 2
Γ ⊢ E : A ⇒ A ⇝ e Γ ⊢ E.l ⇒ A ⇝ e.l Γ ⊢ E 1 , , E 2 ⇒ A 1 & A 2 ⇝ ⟨e 1 , e 2 ⟩
T-rcd
Γ ⊢ E ⇒ A ⇝ e
Γ ⊢{l = E} ⇒{l : A} ⇝ {l = e}
----- End of picture text -----

Figure 5 Bidirectional type system of NeColus.

function types and those for intersection types. It can be shown[5] that the other direction ( A 1 → A 2 & A 3 < : ( A 1 → A 2) & ( A 1 → A 3)) and the contravariant distribution (( A 1 → A 2) & ( A 3 → A 2) < : A 1 & A 3 → A 2) are both derivable from the existing subtyping rules. Rule S-distRcd, which is not found in the original BCD system, prescribes the distribution of records over intersection types. The two distributivity rules are the key to enable nested composition. The rule S-topArr is standard in BCD subtyping, and the new rule S-topRcd plays a similar role for record types.

Non-Algorithmic. The subtyping relation in Fig. 4 is clearly no more than a specification due to the two subtyping axioms: rules S-refl and S-trans. A sound and complete algorithmic version is discussed in Section 5. Nevertheless, for the sake of establishing coherence, the declarative subtyping relation is sufficient.

3.3 Typing of NeColus

The bidirectional type system for NeColus is shown in Fig. 5. Again we ignore the highlighted parts for now.

Typing Rules and Disjointness. As with traditional bidirectional type systems, we employ two modes: the inference mode ( ⇒ ) and the checking mode ( ⇐ ). The inference judgement Γ ⊢ E ⇒ A says that we can synthesize a type A for expression E in the context Γ. The

• 5 The full derivations are found in the appendix.

ECOOP 2018

--- end of page.page_number=11 ---

22:12 The Essence of Nested Composition

D-arr _A_2_∗B_2 _A_1 _→A_2_∗B_1 _→B_2 D-andL A_1_∗B A_2_∗B _A_1&A_2_∗B D-rcdNeq _l_1 =l_2 {l_1 :A} ∗{l_2 :B} D-axNatArr Nat_∗A_1 →A_2 D-axRcdNat {l :_A} ∗_Nat D-axArrRcd _A_1 →A_2_∗{l :A}	(Disjointness) D-andR _A ∗B_1 _A ∗B_2 _A ∗B_1&_B_2 D-axArrNat A_1 →A_2_∗_Nat D-axRcdArr {l :_A} ∗A_1 _→A_2

Figure 6 Disjointness.

|Target types|τ|::=|Nat_| ⟨⟩| τ_1_× τ_2 | τ_1 →τ_2 | {l :τ}| |---|---|---|---| |Typing contexts|∆|::=|• |∆, x :τ| |Target terms|e|::=|x | i | ⟨⟩| λx. e | e_1_e_2 | ⟨e_1, e_2⟩| {l_ =e} | e.l | c e| |Coercions|c|::=|id_| c_1_◦c_2 |top|top_→|top{l} | c_1 →c_2 | ⟨c_1, c_2⟩| ||||_|_π_1 | π_2 | {l :c} |dist{l} |dist_→| |Target values|v|::=|λx. e | ⟨⟩| i | ⟨v_1, v_2⟩|(_c_1 _→c_2)_v |_dist_→v |top_→v|

Figure 7 λc types, terms and coercions.

checking judgement Γ ⊢ E ⇐ A checks E against A in the context Γ. The disjointness judgement A ∗ B used in rule T-merge is shown in Fig. 6, which states that the types A and B are disjoint . The intuition of two types being disjoint is that their least upper bound is (isomorphic to) ⊤ . The disjointness judgement is important in order to rule out ambiguous expressions such as 1 , , 2. Most of the typing and disjointness rules are standard and are explained in detail in previous work [46, 2].

3.4 Elaboration Semantics

The operational semantics of NeColus is given by elaborating source expressions E into target terms e . Our target language λc is the standard simply-typed call-by-value λ -calculus extended with singleton records, products and coercions. The syntax of λc is shown in Fig. 7. The meta-function | · | transforms NeColus types to λc types, and extends naturally to typing contexts. Its definition is in the appendix.

Explicit Coercions and Coercive Subtyping. The separate syntactic category for explicit coercions is a distinct difference from the prior works (in which they are regular terms). Our coercions are based on those of Henglein [32], and we add more forms due to our extra subtyping rules. Metavariable c ranges over coercions.[6] Coercions express the conversion of a term from one type to another. Because of the addition of coercions, the grammar contains explicit coercion applications c e as a term, and various unsaturated coercion applications as values. The use of explicit coercions is useful for the new semantic proof of coherence based

6 Coercions π 1 and π 2 subsume the first and second projection of pairs, respectively.

--- end of page.page_number=12 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:13

(Coercion typing)

c ⊢ τ 1 ▷τ 2 (Coercion cotyp-trans cotyp-refl cotyp-top cotyp-topArr c 1 ⊢ τ 2 ▷τ 3 c 2 ⊢ τ 1 ▷τ 2 id ⊢ τ ▷τ c 1 ◦ c 2 ⊢ τ 1 ▷τ 3 top ⊢ τ ▷ ⟨⟩ top → ⊢⟨⟩ ▷ ⟨⟩→⟨⟩ cotyp-arr cotyp-pair cotyp-topRcd c 1 ⊢ τ 1 [′][▷τ] 1 c 2 ⊢ τ 2 ▷τ 2 [′] c 1 ⊢ τ 1 ▷τ 2 c 2 ⊢ τ 1 ▷τ 3 top {l} ⊢⟨⟩ ▷ {l : ⟨⟩} c 1 → c 2 ⊢ τ 1 → τ 2 ▷τ 1 [′][→][τ][ ′] 2 ⟨c 1 , c 2 ⟩⊢ τ 1 ▷τ 2 × τ 3 cotyp-rcd cotyp-projl cotyp-projr c ⊢ τ 1 ▷τ 2 π 1 ⊢ τ 1 × τ 2 ▷τ 1 π 2 ⊢ τ 1 × τ 2 ▷τ 2 {l : c} ⊢{l : τ 1 } ▷ {l : τ 2 } cotyp-distRcd cotyp-distArr dist {l} ⊢{l : τ 1 } × {l : τ 2 } ▷ {l : τ 1 × τ 2 } dist → ⊢ ( τ 1 → τ 2) × ( τ 1 → τ 3) ▷τ 1 → τ 2 × τ 3

Figure 8 Coercion typing.

on logical relations. The subtyping judgement in Fig. 4 has the form A < : B ⇝ c , which says that the subtyping derivation of A < : B produces a coercion c that converts terms of type |A| to type |B| . Each subtyping rule has its own specific form of coercion.

Target Typing. The typing of λc has the form ∆ ⊢ e : τ , which is entirely standard. Only the typing of coercion applications, shown below, deserves attention:

Here the judgement c ⊢ τ 1 ▷τ 2 expresses the typing of coercions, which are essentially functions from τ 1 to τ 2. Their typing rules correspond exactly to the subtyping rules of NeColus, as shown in Fig. 8.

Target Operational Semantics and Type Safety. The operational semantics of λc is mostly unremarkable. What may be interesting is the operational semantics of coercions. Figure 9 shows the single-step ( −→ ) reduction rules for coercions. Our coercion reduction rules are quite standard but not efficient in terms of space. Nevertheless, there is existing work on space-efficient coercions [60, 33], which should be applicable to our work as well. As standard, −→[∗] is the reflexive, transitive closure of −→ . We show that λc is type safe:

• Theorem 1 (Preservation) . If • ⊢ e : τ and e −→ e[′] , then • ⊢ e[′] : τ .

• Theorem 2 (Progress) . If • ⊢ e : τ , then either e is a value, or ∃e[′] such that e −→ e[′] .

Elaboration. We are now in a position to explain the elaboration judgements Γ ⊢ E ⇒ A ⇝ e and Γ ⊢ E ⇐ A ⇝ e in Fig. 5. The only interesting rule is rule T-sub, which applies the coercion c produced by subtyping to the target term e to form a coercion application c e . All the other rules do straightforward translations between source and target expressions.

To conclude, we show two lemmas that relate NeColus expressions to λc terms.

• Lemma 3 (Coercions preserve types) . If A < : B ⇝ c, then c ⊢|A| ▷ |B|.

ECOOP 2018

--- end of page.page_number=13 ---

22:14 The Essence of Nested Composition

----- Start of picture text -----
e −→ e [′] (Coercion reduction)
step-id step-trans step-top
step-topArr
id v −→ v ( c 1 ◦ c 2) v −→ c 1 ( c 2 v ) top v −→⟨⟩ (top → ⟨⟩ ) ⟨⟩−→⟨⟩
step-pair step-arr
step-topRcd
top {l} ⟨⟩−→{l = ⟨⟩} ⟨c 1 , c 2 ⟩ v −→⟨c 1 v, c 2 v⟩ (( c 1 → c 2) v 1) v 2 −→ c 2 ( v 1 ( c 1 v 2))
step-distArr step-projl step-projr
(dist → ⟨v 1 , v 2 ⟩ ) v 3 −→⟨v 1 v 3 , v 2 v 3 ⟩ π 1 ⟨v 1 , v 2 ⟩−→ v 1 π 2 ⟨v 1 , v 2 ⟩−→ v 2
step-crcd step-distRcd
{l : c} {l = v} −→{l = c v} dist {l} ⟨{l = v 1 }, {l = v 2 }⟩−→{l = ⟨v 1 , v 2 ⟩}
----- End of picture text -----

Figure 9 Coercion reduction.

Proof. By structural induction on the derivation of subtyping.

◀

▶ Lemma 4 (Elaboration soundness) . We have that: If Γ ⊢ E ⇒ A ⇝ e, then | Γ | ⊢ e : |A|. If Γ ⊢ E ⇐ A ⇝ e, then | Γ | ⊢ e : |A|.

Proof. By structural induction on the derivation of typing. ◀

3.5 Comparison with λi

Below we identify major differences between λ[+] i[and] [λ][i][,][which,][when][taken][together,][yield] a simpler and more elegant system. The differences may seem superficial, but they have far-reaching impacts on the semantics, especially on coherence, our major topic in Section 4.

No Ordinary Types. Apart from the extra subtyping rules, there is an important difference from the λi subtyping relation. The subtyping relation of λi employs an auxiliary unary relation called ordinary, which plays a fundamental role for ensuring coherence and obtaining an algorithm [21]. The NeColus calculus discards the notion of ordinary types completely; this yields a clean and elegant formulation of the subtyping relation. Another minor difference is that due to the addition of the transitivity axiom (rule S-trans), rules S-andl and S-andr are simplified: an intersection type A & B is a subtype of both A and B , instead of the more general form A & B < : C .

No Top-Like Types. There is a notable difference from the coercive subtyping of λi . Because of their syntactic proof method, they have special treatment for coercions of top-like types in order to retain coherence. For NeColus, as with ordinary types, we do not need this kind of ad-hoc treatment, thanks to the adoption of a more powerful proof method (cf. Section 4).

No Well-Formedness Judgement. A key difference from the type system of λi is the complete omission of the well-formedness judgement. In λi , the well-formedness judgement

--- end of page.page_number=14 ---

22:15

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

Γ ⊢ A appears in both rules T-abs and T-sub. The sole purpose of this judgement is to enforce the invariant that all intersection types are disjoint. However, as Section 4 will explain, the syntactic restriction is unnecessary for coherence, and merely complicates the type system. The NeColus calculus discards this well-formedness judgement altogether in favour of a simpler design that is still coherent. An important implication is that even without adding BCD subtyping, NeColus is already more expressive than λi : an expression such as 1 : Nat & Nat is accepted in NeColus but rejected in λi . This simplification is based on an important observation: incoherence can only originate in merges. Therefore disjointness checking is only necessary in rule T-merge.

4 Coherence

This section constructs logical relations to establish the coherence of NeColus. Finding a suitable definition of coherence for NeColus is already challenging in its own right. In what follows we reproduce the steps of finding a definition for coherence that is both intuitive and applicable. Then we present the construction of logical (equivalence) relations tailored to this definition, and the connection between logical equivalence and coherence.

4.1 In Search of Coherence

In λi the definition of coherence is based on α -equivalence. More specifically, their coherence property states that any two target terms that a source expression elaborates into must be exactly the same (up to α -equivalence). Unfortunately this syntactic notion of coherence is very fragile with respect to extensions. For example, it is not obvious how to retain this notion of coherence when adding more subtyping rules such as those in Fig. 4.

If we permit ourselves to consider only the syntactic aspects of expressions, then very few expressions can be considered equal. The syntactic view also conflicts with the intuition that the significance of an expression lies in its contribution to the outcome of a computation [31]. Drawing inspiration from a wide range of literature on contextual equivalence [41], we want a context-based notion of coherence. It is helpful to consider several examples before presenting the formal definition of our new semantically founded notion of coherence.

▶ Example 5. The same NeColus expression 3 can be typed Nat in many ways: for instance, by rule T-lit; by rules T-sub and S-refl; or by rules T-sub, S-trans, and S-refl, resulting in λc terms 3, id 3 and (id ◦ id) 3, respectively. It is apparent that these three λc terms are “equal” in the sense that all reduce to the same numeral 3.

Expression Contexts and Contextual Equivalence. To formalize the intuition, we introduce the notion of expression contexts . An expression context D is a term with a single hole [ · ] (possibly under some binders) in it. The syntax of λc expression contexts can be found in Fig. 10. The typing judgement for expression contexts has the form D : (∆ ⊢ τ ) ⇝ (∆ [′] ⊢ τ[′] ) where (∆ ⊢ τ ) indicates the type of the hole. This judgement essentially says that plugging a well-typed term ∆ ⊢ e : τ into the context D gives another well-typed term ∆ [′] ⊢D{e} : τ[′] . We define a complete program to mean any closed term of type Nat. The following two definitions capture the notion of contextual equivalence .

▶ Definition 6 (Kleene Equality) . Two complete programs, e and e[′] , are Kleene equal, written e ⋍ e[′] , iff there exists i such that e −→[∗] i and e[′] −→[∗] i .

▶ Definition 7 ( λc Contextual Equivalence) .

ECOOP 2018

--- end of page.page_number=15 ---

22:16 The Essence of Nested Composition

λc contexts D ::= [ · ] | λx. D | D e 2 | e 1 D | ⟨D, e 2 ⟩| ⟨e 1 , D⟩| c D | {l = D} | D.l NeColus contexts C ::= [ · ] | λx. C | C E 2 | E 1 C | E 1 , , C | C , , E 2 | C : A | {l = C} | C.l

Figure 10 Expression contexts of NeColus and λc .

Regarding Example 5, it seems adequate to say that 3 and id 3 are contextually equivalent. Does this imply that coherence can be based on Definition 7? Unfortunately it cannot, as demonstrated by the following example.

▶ Example 8. It may be counter-intuitive that two λc terms λx. π 1 x and λx. π 2 x should also be considered equal. To see why, first note that they are both translations of the same NeColus expression: ( λx. x ) : Nat & Nat → Nat. What can we do with this lambda abstraction? We can apply it to 1 : Nat & Nat for example. In that case, we get two translations ( λx. π 1 x ) ⟨ 1 , 1 ⟩ and ( λx. π 2 x ) ⟨ 1 , 1 ⟩ , which both reduce to the same numeral 1. However, λx. π 1 x and λx. π 2 x are definitely not equal according to Definition 7, as one can find a context [ · ] ⟨ 1 , 2 ⟩ where the two terms reduce to two different numerals. The problem is that not every well-typed λc term can be obtained from a well-typed NeColus expression through the elaboration semantics. For example, [ · ] ⟨ 1 , 2 ⟩ should not be considered because the (non-disjoint) source expression 1 , , 2 is rejected by the type system of the source calculus NeColus and thus never gets elaborated into ⟨ 1 , 2 ⟩ .

NeColus Contexts and Refined Contextual Equivalence. Example 8 hints at a shift from λc contexts to NeColus contexts C , whose syntax is shown in Fig. 10. Due to the bidirectional nature of the type system, the typing judgement of C features 4 different forms:

We write C : (Γ ⇔ A ) �→ (Γ [′] ⇔[′] A[′] ) ⇝ D to abbreviate the above 4 different forms. Take C : (Γ ⇒ A ) �→ (Γ [′] ⇒ A[′] ) ⇝ D for example, it reads given a well-typed NeColus expression Γ ⊢ E ⇒ A , we have Γ [′] ⊢C{E} ⇒ A[′] . The judgement also generates a λc context D such that D : ( | Γ | ⊢|A| ) ⇝ ( | Γ [′] | ⊢|A[′] | ) holds by construction. The typing rules appear in the appendix. Now we are ready to refine Definition 7’s contextual equivalence to take into consideration both NeColus and λc contexts.

▶ Definition 9 (NeColus Contextual Equivalence) .

▶ Remark. For brevity we only consider expressions in the inference mode. Our Coq formalization is complete with two modes.

Regarding Example 8, a possible NeColus context is [ · ] 1 : ( • ⇒ Nat & Nat → Nat) �→ ( • ⇒ Nat) ⇝ [ · ] ⟨ 1 , 1 ⟩ . We can verify that both λx. π 1 x and λx. π 2 x produce 1 in the context [ · ] ⟨ 1 , 1 ⟩ . Of course we should consider all possible contexts to be certain they are truly equal. From now on, we use the symbol ⋍ ctx to refer to contextual equivalence in Definition 9. With Definition 9 we can formally state that NeColus is coherent in the following theorem:

--- end of page.page_number=16 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:17

( v 1 , v 2) ∈V �Nat; Nat� ≜ ∃i, v 1 = v 2 = i

( v 1 , v 2) ∈V � τ 1 → τ 2; τ 1 [′][→][τ][ ′] 2[�][≜] [∀][(] [v][,][ v][′][)] [ ∈V][�] [τ] 1[;] [ τ][ ′] 1[�] [,][ (] [v] 1 [v][,][ v] 2 [v][′][)] [ ∈E][�] [τ] 2[;] [ τ][ ′] 2[�]

( {l = v 1 }, {l = v 2 } ) ∈V � {l : τ 1 } ; {l : τ 2 } � ≜ ( v 1 , v 2) ∈V � τ 1; τ 2�

( ⟨v 1 , v 2 ⟩, v 3) ∈V � τ 1 × τ 2; τ 3� ≜ ( v 1 , v 3) ∈V � τ 1; τ 3� ∧ ( v 2 , v 3) ∈V � τ 2; τ 3�

( v 3 , ⟨v 1 , v 2 ⟩ ) ∈V � τ 3; τ 1 × τ 2� ≜ ( v 3 , v 1) ∈V � τ 3; τ 1� ∧ ( v 3 , v 2) ∈V � τ 3; τ 2�

( v 1 , v 2) ∈V � τ 1; τ 2� ≜ true otherwise

( e 1 , e 2) ∈E � τ 1; τ 2� ≜ ∃v 1 v 2 , e 1 −→[∗] v 1 ∧ e 2 −→[∗] v 2 ∧ ( v 1 , v 2) ∈V � τ 1; τ 2�

Figure 11 Logical relations for λc .

For the same reason as in Definition 9, we only consider expressions in the inference mode. The rest of the section is devoted to proving that Theorem 10 holds.

4.2 Logical Relations

Intuitive as Definition 9 may seem, it is generally very hard to prove contextual equivalence directly, since it involves quantification over all possible contexts. Worse still, two kinds of contexts are involved in Theorem 10, which makes reasoning even more tedious. The key to simplifying the reasoning is to exploit types by using logical relations [63, 61, 48].

In Search of a Logical Relation. It is worth pausing to ponder what kind of relation we are looking for. The high-level intuition behind the relation is to capture the notion of “coherent” values. These values are unambiguous in every context. A moment of thought leads us to the following important observations:

▶ Observation 1 (Disjoint values are unambiguous). The relation should relate values originating from disjoint intersection types. Those values are essentially translated from merges, and since rule T-merge ensures disjointness, they are unambiguous. For example, ⟨ 1 , {l = 1 }⟩ corresponds to the type Nat & {l : Nat } . It is always clear which one to choose (1 or {l = 1 } ) no matter how this pair is used in certain contexts.

▶ Observation 2 (Duplication is unambiguous). The relation should relate values originating from non-disjoint intersection types, only if the values are duplicates. This may sound baffling since the whole point of disjointness is to rule out (ambiguous) expressions such as 1 , , 2. However, 1 , , 2 never gets elaborated, and the only values corresponding to Nat & Nat are those pairs such as ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ , etc. Those values are essentially generated from rule T-sub and are also unambiguous.

To formalize values being “coherent” based on the above observations, Figure 11 defines two (binary) logical relations for λc , one for values ( V � τ 1; τ 2�) and one for terms ( E � τ 1; τ 2�). We require that any two values ( v 1 , v 2) ∈V � τ 1; τ 2� are closed and well-typed. For succinctness, we write V � τ � to mean V � τ ; τ �, and similarly for E � τ �.

▶ Remark. The logical relations are heterogeneous, parameterized by two types, one for each argument. This is intended to relate values of different types.

▶ Remark. The logical relations resemble those given by Biernacki and Polesiuk [8], as both are heterogeneous. However, two important differences are worth pointing out. Firstly, our

ECOOP 2018

--- end of page.page_number=17 ---

22:18 The Essence of Nested Composition

value relation for product types ( V � τ 1 × τ 2; τ 3� and V � τ 3; τ 1 × τ 2�) is unusual. Secondly, their value relation disallows relating functions with natural numbers, while ours does not. As we explain shortly, both points are related to disjointness.

First let us consider V � τ 1; τ 2�. The first three cases are standard: Two natural numbers are related iff they are the same numeral. Two functions are related iff they map related arguments to related results. Two singleton records are related iff they have the same label and their fields are related. These cases reflect Observation 2: the same type corresponds to the same value.

In the next two cases one of the parameterized types is a product type. In those cases, the relation distributes over the product constructor × . This may look strange at first, since the traditional way of relating pairs is by relating their components pairwise. That is, ⟨v 1 , v 2 ⟩ and ⟨v 1 [′][,][ v] 2 [′][⟩][are][related][iff][(1)] [v][1][and] [v] 1 [′][are][related][and][(2)] [v][2][and] [v] 2 [′][are][related.][According] to our definition, we also require that (3) v 1 and v 2 [′][are][related][and][(4)] [v][2][and] [v] 1 [′][are][related.] The design of these two cases is influenced by the disjointness of intersection types. Below are two rules dealing with intersection types:

Notice the structural similarity between these two rules and the two cases. Now it is clear that the cases for products manifests disjointness of intersection types, reflecting Observation 1. Together with the last case, we can show that disjointness and the value relation are connected by the following lemma:

▶ Lemma 11 (Disjoint values are in a value relation) . If A 1 ∗ A 2 and v 1 : |A 1 | and v 2 : |A 2 |, then ( v 1 , v 2) ∈V � |A 1 | ; |A 2 | � .

Proof. By induction on the derivation of disjointness.

◀

Next we consider E � τ 1; τ 2�, which is standard. Informally it expresses that two closed terms e 1 and e 2 are related iff they evaluate to two values v 1 and v 2 that are related.

Logical Equivalence. The logical relations can be lifted to open terms in the usual way. First we give the semantic interpretation of typing contexts:

▶ Definition 12 (Interpretation of Typing Contexts) . ( γ 1 , γ 2) ∈G �∆1; ∆2� is defined as follows:

Two open terms are related if every pair of related closing substitutions makes them related:

▶ Definition 13 (Logical equivalence) . Let ∆1 ⊢ e 1 : τ 1 and ∆2 ⊢ e 2 : τ 2.

For succinctness, we write ∆ ⊢ e 1 ⋍ log e 2 : τ to mean ∆; ∆ ⊢ e 1 ⋍ log e 2 : τ ; τ .

--- end of page.page_number=18 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:19

4.3 Establishing Coherence

With all the machinery in place, we are now ready to prove Theorem 10. But we need several lemmas to set the stage.

First we show compatibility lemmas, which state that logical equivalence is preserved by every language construct. Most are standard and thus are omitted. We show only one compatibility lemma that is specific to our relations:

▶ Lemma 14 (Coercion Compatibility) . Suppose that c ⊢ τ 1 ▷τ 2 , If ∆1; ∆2 ⊢ e 1 ⋍ log e 2 : τ 1; τ 0 then ∆1; ∆2 ⊢ c e 1 ⋍ log e 2 : τ 2; τ 0 . If ∆1; ∆2 ⊢ e 1 ⋍ log e 2 : τ 0; τ 1 then ∆1; ∆2 ⊢ e 1 ⋍ log c e 2 : τ 0; τ 2 .

Proof. By induction on the typing derivation of the coercion c . ◀

The “Fundamental Property” states that any well-typed expression is related to itself by the logical relation. In our elaboration setting, we rephrase it so that any two λc terms elaborated from the same NeColus expression are related by the logical relation. To prove it, we require Theorem 15.

• Theorem 15 (Inference Uniqueness) . If Γ ⊢ E ⇒ A 1 and Γ ⊢ E ⇒ A 2 , then A 1 ≡ A 2 .

• Theorem 16 (Fundamental Property) . We have that: If Γ ⊢ E ⇒ A ⇝ e and Γ ⊢ E ⇒ A ⇝ e[′] , then | Γ | ⊢ e ⋍ log e[′] : |A|. If Γ ⊢ E ⇐ A ⇝ e and Γ ⊢ E ⇐ A ⇝ e[′] , then | Γ | ⊢ e ⋍ log e[′] : |A|.

Proof. The proof follows by induction on the first derivation. The most interesting case is rule T-sub where we need Theorem 15 to be able to apply the induction hypothesis. Then we apply Lemma 14 to say that the coercion generated preserves the relation between terms. For the other cases we use the appropriate compatibility lemmas. ◀

▶ Remark. It is interesting to ask whether the Fundamental Property holds in the target language. That is, if ∆ ⊢ e : τ then ∆ ⊢ e ⋍ log e : τ . Clearly this does not hold for every well-typed λc term. However, as we have emphasized, we do not need to consider every λc term. Our logical relation is carefully formulated so that the Fundamental Property holds in the source language.

We show that logical equivalence is preserved by NeColus contexts:

▶ Lemma 17 (Congruence) . If C : (Γ ⇔ A ) �→ (Γ [′] ⇔[′] A[′] ) ⇝ D, Γ ⊢ E 1 ⇔ A ⇝ e 1 , Γ ⊢ E 2 ⇔ A ⇝ e 2 and | Γ | ⊢ e 1 ⋍ log e 2 : |A|, then | Γ [′] | ⊢D{e 1 } ⋍ log D{e 2 } : |A[′] |.

Proof. By induction on the typing derivation of the context C , and applying the compatibility lemmas where appropriate. ◀

• Lemma 18 (Adequacy) . If • ⊢ e 1 ⋍ log e 2 : Nat then e 1 ⋍ e 2 .

Proof. Adequacy follows easily from the definition of the logical relation. ◀

Next up is the proof that logical relation is sound with respect to contextual equivalence:

▶ Theorem 19 (Soundness w.r.t. Contextual Equivalence) . If Γ ⊢ E 1 ⇒ A ⇝ e 1 and Γ ⊢ E 2 ⇒ A ⇝ e 2 and | Γ | ⊢ e 1 ⋍ log e 2 : |A| then Γ ⊢ E 1 ⋍ ctx E 2 : A.

Proof. From Definition 9, we are given a context C : (Γ ⇒ A ) �→ ( • ⇒ Nat) ⇝ D . By Lemma 17 we have • ⊢D{e 1 } ⋍ log D{e 2 } : Nat, thus D{e 1 } ⋍ D{e 2 } by Lemma 18. ◀

ECOOP 2018

--- end of page.page_number=19 ---

22:20 The Essence of Nested Composition

Armed with Theorem 16 and Theorem 19, coherence follows directly.

▶ Theorem 10 (Coherence) . If Γ ⊢ E ⇒ A then Γ ⊢ E ⋍ ctx E : A.

Proof. Immediate from Theorem 16 and Theorem 19.

◀

4.4 Some Interesting Corollaries

To showcase the strength of the new proof method, we can derive some interesting corollaries. For the most part, they are direct consequences of logical equivalence which carry over to contextual equivalence.

Corollary 20 says that merging a term of some type with something else does not affect its semantics. Corollary 21 and Corollary 22 express that merges are commutative and associative, respectively. Corollary 23 states that coercions from the same types are “coherent”.

▶ Corollary 20 (Merge is Neutral) . If Γ ⊢ E 1 ⇒ A and Γ ⊢ E 1 , , E 2 ⇒ A, then Γ ⊢ E 1 ⋍ ctx E 1 , , E 2 : A

▶ Corollary 21 (Merge is Commutative) . If Γ ⊢ E 1 , , E 2 ⇒ A and Γ ⊢ E 2 , , E 1 ⇒ A, then Γ ⊢ E 1 , , E 2 ⋍ ctx E 2 , , E 1 : A.

▶ Corollary 22 (Merge is Associative) . If Γ ⊢ ( E 1 , , E 2) , , E 3 ⇒ A and Γ ⊢ E 1 , , ( E 2 , , E 3) ⇒ A, then Γ ⊢ ( E 1 , , E 2) , , E 3 ⋍ ctx E 1 , , ( E 2 , , E 3) : A.

▶ Corollary 23 (Coercions Preserve Semantics) . If A < : B ⇝ c 1 and A < : B ⇝ c 2 , then ∆ ⊢ λx. c 1 x ⋍ log λx. c 2 x : |A| →|B|.

5 Algorithmic Subtyping

This section presents an algorithm that implements the subtyping relation in Fig. 4. While BCD subtyping is well-known, the presence of a transitivity axiom in the rules means that the system is not algorithmic. This raises an obvious question: how to obtain an algorithm for this subtyping relation? Laurent [37] has shown that simply dropping the transitivity rule from the BCD system is not possible without losing expressivity. Hence, this avenue for obtaining an algorithm is not available. Instead, we adapt Pierce’s decision procedure [47] for a subtyping system (closely related to BCD) to obtain a sound and complete algorithm for our BCD extension. Our algorithm extends Pierce’s decision procedure with subtyping of singleton records and coercion generation. We prove in Coq that the algorithm is sound and complete with respect to the declarative version. At the same time we find some errors and missing lemmas in Pierce’s original manual proofs.

5.1 The Subtyping Algorithm

Figure 12 shows the algorithmic subtyping judgement L ⊢ A ≺ : B ⇝ c . This judgement is the algorithmic counterpart of the declarative judgement A < : L → B ⇝ c , where the symbol L stands for a queue of types and labels. Definition 24 converts a queue to a type:

• Definition 24. L → A is inductively defined as follows:

[] → A = A ( L, B ) → A = L → ( B → A ) ( L, {l} ) → A = L →{l : A}

--- end of page.page_number=20 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:21

Figure 12 Algorithmic subtyping of NeColus.

For instance, if L = A, B, {l} , then L → C abbreviates A → B →{l : C} .

The basic idea of L ⊢ A ≺ : B ⇝ c is to first perform a structural analysis of B , which descends into both sides of & ’s (rule A-and), into the right side of → ’s (rule A-arr), and into the fields of records (rule A-rcd) until it reaches one of the two base cases, Nat or ⊤ . If the base case is ⊤ , then the subtyping holds trivially (rule A-top). If the base case is Nat, the algorithm performs a structural analysis of A , in which L plays an important role. The left sides of → ’s are pushed onto L as they are encountered in B and popped off again later, left to right, as → ’s are encountered in A (rule A-arrNat). Similarly, the labels are pushed onto L as they are encountered in B and popped off again later, left to right, as records are encountered in A (rule A-rcdNat). The remaining rules are similar to their declarative counterparts. Let us illustrate the algorithm with an example derivation (for space reasons we use N and S to denote Nat and String respectively), which is essentially the one used by the add field in Section 2. The readers can try to give a corresponding derivation using the declarative subtyping and see how rule S-trans plays an essential role there.

where the sub-derivation D is shown below ( D[′] is similar):

Now consider the coercions. Algorithmic subtyping uses the same set of coercions as declarative subtyping. However, because algorithmic subtyping has a different structure, the rules generate slightly more complicated coercions. Two meta-functions � · � ⊤ and � · �& used in rules A-top and A-and respectively, are meant to generate correct forms of coercions. They are defined recursively on L and are shown in Fig. 13.

ECOOP 2018

--- end of page.page_number=21 ---

22:22 The Essence of Nested Composition

Figure 13 Meta-functions of coercions.

5.2 Correctness of the Algorithm

To establish the correctness of the algorithm, we must show that the algorithm is both sound and complete with respect to the declarative specification. While soundness follows quite easily, completeness is much harder. The proof of completeness essentially follows that of Pierce [47] in that we need to show the algorithmic subtyping is reflexive and transitive.

Soundness of the Algorithm. The proof of soundness is straightforward.

▶ Theorem 25 (Soundness) . If L ⊢ A ≺ : B ⇝ c then A < : L → B ⇝ c.

Proof. By induction on the derivation of the algorithmic subtyping. ◀

Completeness of the Algorithm. Completeness, however, is much harder. The reason is that, due to the use of L , reflexivity and transitivity are not entirely obvious. We need to strengthen the induction hypothesis by introducing the notion of a set, U ( A ), of “reflexive supertypes” of A , as defined below:

We show two lemmas about U ( A ) that are crucial in the subsequent proofs.

▶ Lemma 26. A ∈U ( A )

Proof. By induction on the structure of A . ◀

▶ Lemma 27. If A ∈U ( B ) and B ∈U ( C ) , then A ∈U ( C ) .

Proof. By induction on the structure of B . ◀

▶ Remark. Lemma 27 is not found in Pierce’s proofs [47], which is crucial in Lemma 28, from which reflexivity (Lemma 29) follows immediately.

▶ Lemma 28. If L → B ∈U ( A ) then there exists c such that L ⊢ A ≺ : B ⇝ c.

Proof. By induction on size( A ) + size( B ) + size( L ). ◀

Now it immediately follows that the algorithmic subtyping is reflexive.

▶ Lemma 29 (Reflexivity) . For every A there exists c such that [] ⊢ A ≺ : A ⇝ c.

Proof. Immediate from Lemma 26 and Lemma 28. ◀

We omit the details of the proof of transitivity.

▶ Lemma 30 (Transitivity) . If [] ⊢ A 1 ≺ : A 2 ⇝ c 1 and [] ⊢ A 2 ≺ : A 3 ⇝ c 2 , then there exists c such that [] ⊢ A 1 ≺ : A 3 ⇝ c.

--- end of page.page_number=22 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:23

With reflexivity and transitivity in position, we show the main theorem.

▶ Theorem 31 (Completeness) . If A < : B ⇝ c then there exists c[′] such that [] ⊢ A ≺ : B ⇝ c[′] .

Proof. By induction on the derivation of the declarative subtyping and applying Lemmas 29 and 30 where appropriate. ◀

▶ Remark. Pierce’s proof is wrong [47, pp. 20, Case F] in the case

where he concludes from the inductive hypotheses [] ⊢ B 1 ≺ : A 1 and [] ⊢ A 2 ≺ : B 2 that [] ⊢ A 1 → A 2 ≺ : B 1 → B 2 (rules 6a and 3). However his rule 6a (our rule A-arrNat) only works for primitive types , and is thus not applicable in this case. Instead we need a few technical lemmas to support the argument.

▶ Remark. It is worth pointing out that the two coercions c and c[′] in Theorem 31 are contextually equivalent, which follows from Theorem 25 and Corollary 23.

6 Related Work

Coherence. In calculi that feature coercive subtyping, a semantics that interprets the subtyping judgement by introducing explicit coercions is typically defined on typing derivations rather than on typing judgements. A natural question that arises for such systems is whether the semantics is coherent , i.e., distinct typing derivations of the same typing judgement possess the same meaning. Since Reynolds [55] proved the coherence of a calculus with intersection types, based on the denotational semantics for intersection types, many researchers have studied the problem of coherence in a variety of typed calculi. Below we summarize two commonly-found approaches in the literature.

Breazu-Tannen et al. [10] proved the coherence of a coercion translation from Fun [13] extended with recursive types to System F by showing that any two typing derivations of the same judgement are normalizable to a unique normal derivation. Ghelli [20] presented a translation of System F ≤ into a calculus with explicit coercions and showed that any derivations of the same judgement are translated to terms that are normalizable to a unique normal form. Following the same approach, Schwinghammer [59] proved the coherence of coercion translation from Moggi’s computational lambda calculus [40] with subtyping.

Central to the first approach is to find a normal form for a representation of the derivation and show that normal forms are unique for a given typing judgement. However, this approach cannot be directly applied to Curry-style calculi, i.e, where the lambda abstractions are not type annotated. Also this line of reasoning cannot be used when the calculus has general recursion. Biernacki and Polesiuk [8] considered the coherence problem of coercion semantics. Their criterion for coherence of the translation is contextual equivalence in the target calculus. They presented a construction of logical relations for establishing so constructed coherence for coercion semantics, applicable in a variety of calculi, including delimited continuations and control-effect subtyping.

As far as we know, our work is the first to use logical relations to show the coherence for intersection types and the merge operator. The BCD subtyping in our setting poses a non-trivial complication over Biernacki and Polesiuk’s simple structural subtyping. Indeed, because any two coercions between given types are behaviorally equivalent in the target language, their coherence reasoning can all take place in the target language. This is not

ECOOP 2018

--- end of page.page_number=23 ---

22:24 The Essence of Nested Composition

true in our setting, where coercions can be distinguished by arbitrary target programs, but not those that are elaborations of source programs. Hence, we have to restrict our reasoning to the latter class, which is reflected in a more complicated notion of contextual equivalence and our logical relation’s non-trivial treatment of pairs.

Intersection Types and the Merge Operator. Forsythe [54] has intersection types and a merge-like operator. However to ensure coherence, various restrictions were added to limit the use of merges. For example, in Forsythe merges cannot contain more than one function. Castagna et al. [15] proposed a coherent calculus with a special merge operator that works on functions only. More recently, Dunfield [23] shows significant expressiveness of type systems with intersection types and a merge operator. However his calculus lacks coherence. The limitation was addressed by Oliveira et al. [46], who introduced disjointness to ensure coherence. The combination of intersection types, a merge operator and parametric polymorphism, while achieving coherence was first studied in the Fi calculus [2]. Compared to prior work, NeColus simplifies type systems with disjoint intersection types by removing several restrictions. Furthermore, NeColus adopts a more powerful subtyping relation based on BCD subtyping, which in turn requires the use of a more powerful logical relations based method for proving coherence.

BCD Type System and Decidability. The BCD type system was first introduced by Barendregt et al. [4]. It is derived from a filter lambda model in order to characterize exactly the strongly normalizing terms. The BCD type system features a powerful subtyping relation, which serves as a base for our subtyping relation. Bessai el at. [5] showed how to type classes and mixins in a BCD-style record calculus with Bracha-Cook’s merge operator [9]. Their merge can only operate on records, and they only study a type assignment system. The decidability of BCD subtyping has been shown in several works [47, 35, 52, 62]. Laurent [36] has formalized the relation in Coq in order to eliminate transitivity cuts from it, but his formalization does not deliver an algorithm. Based on Statman’s work [62], Bessai et al. [6] show a formally verified subtyping algorithm in Coq. Our Coq formalization follows a different idea based on Pierce’s decision procedure [47], which is shown to be easily extensible to coercions and records. In the course of our mechanization we identified several mistakes in Pierce’s proofs, as well as some important missing lemmas.

Family Polymorphism. There has been much work on family polymorphism since Ernst’s original proposal [25]. Family polymorphism provides an elegant solution to the Expression Problem. Although a simple Scala solution does exist without requiring family polymorphism (e.g., see Wang and Oliveira [65]), Scala does not support nested composition: programmers need to manually compose all the classes from multiple extensions. Generally speaking, systems that support family polymorphism usually require quite sophisticated mechanisms such as dependent types.

There are two approaches to family polymorphism: the original object family approach of Beta (e.g., virtual classes [38]) treats nested classes as attributes of objects of the family classes. Path-dependent types are used to ensure type safety for virtual types and virtual classes in the calculus vc [27]. As for conflicts, vc follows the mixin-style by allowing the rightmost class to take precedence. This is in contrast to NeColus where conflicts are detected statically and resolved explicitly. In the class family approach of Concord [34], Jx and J& [42, 43], nested classes and types are attributes of the family classes directly. Jx supports nested inheritance , a class family mechanism that allows nesting of arbitrary depth. J& is a language that supports nested intersection , building on top of Jx. Similar to NeColus,

--- end of page.page_number=24 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:25

intersection types play an important role in J&, which are used to compose packages/classes. Unlike NeColus, J& does not have a merge-like operator. When conflicts arise, prefix types can be exploited to resolve the ambiguity. J& s [50] is an extension of the Java language that adds class sharing to J&. Saito et al. [57] identified a minimal, lightweight set of language features to enable family polymorphism, Corradi et al. [19] present a language design that integrates modular composition and nesting of Java-like classes. It features a set of composition operators that allow to manipulate nested classes at any depth level. More recently, a Java-like language called Familia [66] were proposed to combine subtyping polymorphism, parametric polymorphism and family polymorphism. The object and class family approaches have even been combined by the work on Tribe [16].

Compared with those systems, which usually focus on getting a relatively complex Javalike language with family polymorphism, NeColus focuses on a minimal calculus that supports nested composition. NeColus shows that a calculus with the merge operator and a variant of BCD captures the essence of nested composition. Moreover NeColus enables new insights on the subtyping relations of families. NeColus’s goal is not to support full family polymorphism which, besides nested composition, also requires dealing with other features such as self types [12, 56] and mutable state. Supporting these features is not the focus of this paper, but we expect to investigate those features in the future.

7 Conclusions and Future Work

We have proposed NeColus, a type-safe and coherent calculus with disjoint intersection types, and support for nested composition/subtyping. It improves upon earlier work with a more flexible notion of disjoint intersection types, which leads to a clean and elegant formulation of the type system. Due to the added flexibility we have had to employ a more powerful proof method based on logical relations to rigorously prove coherence. We also show how NeColus supports essential features of family polymorphism, such as nested composition. We believe NeColus provides insights into family polymorphism, and has potential for practical applications for extensible software designs.

A natural direction for future work is to enrich NeColus with parametric polymorphism. There is abundant literature on logical relations for parametric polymorphism [53]. The main challenge in the definition of the logical relation is the clause that relates type variables with arbitrary types. Careful measures are to be taken to avoid potential circularity due to impredicativity.[7] With the combination of parametric polymorphism and nested composition, an interesting application that we intend to investigate is native support for a highly modular form of Object Algebras [45, 7] and Visitors (or the finally tagless approach [14]).

Another direction for future work is to add mutable references, which would affect two aspects of our metatheory: type safety and coherence. For type safety, we expect that lessons learned from previous work on family polymorphism and mutability on OO apply to our work. For example, it is well-known that subtyping in the presence of mutable state often needs restrictions. Given such suitable restrictions we expect that type-safety in the presence of mutability still holds. For coherence, it would be a major technical challenge to adjust our coherence proof and its Coq mechanization: logical relations that account for mutable state (e.g., see Ahmed’s thesis [1]) introduce significant complexity.

7 Our prototype implementation already supports polymorphism, but we are still in the process of extending our Coq development with polymorphism.

ECOOP 2018

--- end of page.page_number=25 ---

22:26 The Essence of Nested Composition

References

• 1 Amal Jamil Ahmed. Semantics of types for mutable state . PhD thesis, Princeton University, 2004.

• 2 João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European Symposium on Programming , 2017.

• 3 Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In Workshop on Foundations of Object-Oriented Languages , 2012.

• 4 Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The journal of symbolic logic , 48(04):931– 940, 1983.

• 5 Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de’Liguoro. Typing classes and mixins with intersection types. In Workshop on Intersection Types and Related Systems (ITRS) , 2014.

• 6 Jan Bessai, Andrej Dudenhefner, Boris Düdder, and Jakob Rehof. Extracting a formally verified subtyping algorithm for intersection types from ideals and filters. In TYPES , 2016.

• 7 Xuan Bi and Bruno C. d. S. Oliveira. Typed first-class traits. In European Conference on Object-Oriented Programming , 2018.

• 8 Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping. In LIPIcs , 2015.

• 9 Gilad Bracha and William R. Cook. Mixin-based inheritance. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 1990.

• 10 Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation , 93(1):172–221, 1991.

• 11 Kim Bruce, Luca Cardelli, Giuseppe Castagna, Gary T Leavens, Benjamin Pierce, et al. On binary methods. In Theory and Practice of Object Systems , 1996.

• 12 Kim B. Bruce, Angela Schuett, and Robert van Gent. Polytoil: A type-safe polymorphic object-oriented language. In European Conference on Object-Oriented Programming , 1995.

• 13 Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys , 17(4):471–523, 1985.

• 14 Jacques Carette, Oleg Kiselyov, and Chung-Chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming , 19(05):509, 2009.

• 15 Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In LFP , 1992.

• 16 David Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. Tribe: More Types for Virtual Classes. In AOSD , 2007.

• 17 Adriana B Compagnoni and Benjamin C Pierce. Higher-order intersection types and multiple inheritance. MSCS , 6(5):469–501, 1996.

• 18 Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly , 1981.

• 19 Andrea Corradi, Marco Servetto, and Elena Zucca. DeepFJig — modular composition of nested classes. The Journal of Object Technology , 11(2):1:1, 2012.

• 20 Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in f ≤ . MSCS , 2(01):55, 1992.

• 21 Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming , 2000.

• 22 Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew P Black. Traits: A mechanism for fine-grained reuse. ACM Transactions on Programming Languages and Systems (TOPLAS) , 28(2):331–388, 2006.

--- end of page.page_number=26 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:27

• 23 Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming , 24:133–165, 2014.

• 24 Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Foundations of Software Science and Computation Structure (FoSSaCS) , 2003.

• 25 Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming , 2001.

• 26 Erik Ernst. Higher-order hierarchies. In European Conference on Object-Oriented Programming , 2003.

• 27 Erik Ernst, Klaus Ostermann, and William R. Cook. A virtual class calculus. In Symposium on Principles of Programming Languages , 2006.

• 28 Facebook. Flow. https://flow.org/ , 2014.

• 29 Kathleen Fisher and John Reppy. A typed calculus of traits. In Workshop on Foundations of Object-Oriented Languages , 2004.

• 30 Tim Freeman and Frank Pfenning. Refinement types for ML. In Conference on Programming Language Design and Implementation , 1991.

• 31 Robert Harper. Practical Foundations for Programming Languages . Cambridge University Press, 2016.

• 32 Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming , 22(3):197–230, jun 1994.

• 33 David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. HigherOrder and Symbolic Computation , 23(2):167, 2010.

• 34 Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and Klaus Ostermann. Simple dependent types: Concord. In European Conference on Object-Oriented Programming Workshop on Formal Techniques for Java Programs (FTfJP) , 2004.

• 35 Toshihiko Kurata and Masako Takahashi. Decidable properties of intersection type systems. Typed Lambda Calculi and Applications , pages 297–311, 1995.

• 36 Olivier Laurent. Intersection types with subtyping by means of cut elimination. Fundamenta Informaticae , 121(1-4):203–226, 2012.

• 37 Olivier Laurent. A syntactic introduction to intersection types. Unpublished note, 2012.

• 38 O. L. Madsen and B. Moller-Pedersen. Virtual classes: a powerful mechanism in objectoriented programming. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 1989.

• 39 Microsoft. Typescript. https://www.typescriptlang.org/ , 2012.

• 40 Eugenio Moggi. Notions of computation and monads. Information and Computation , 93(1):55–92, 1991.

• 41 James Hiram Morris Jr. Lambda-calculus models of programming languages . PhD thesis, Massachusetts Institute of Technology, 1969.

• 42 Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. Scalable extensibility via nested inheritance. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 2004.

• 43 Nathaniel Nystrom, Xin Qi, and Andrew C. Myers. J&: Nested Intersection for Scalable Software Composition. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 2006.

• 44 Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview of the scala programming language. Technical report, EPFL, 2004.

• 45 Bruno C. d. S. Oliveira and William R. Cook. Extensibility for the masses. In European Conference on Object-Oriented Programming , 2012.

ECOOP 2018

--- end of page.page_number=27 ---

22:28 The Essence of Nested Composition

• 46 Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In International Conference on Functional Programming , 2016.

• 47 Benjamin C Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical report, Carnegie Mellon University, 1989.

• 48 Gordon Plotkin. Lambda-definability and logical relations . Edinburgh University, 1973.

• 49 Garrel Pottinger. A type assignment for the strongly normalizable λ -terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism , 1980.

• 50 Xin Qi and Andrew C. Myers. Sharing classes between families. In Conference on Programming Language Design and Implementation , 2009.

• 51 Redhat. Ceylon. https://ceylon-lang.org/ , 2011.

• 52 Jakob Rehof and Paweł Urzyczyn. Finite combinatory logic with intersection types. In International Conference on Typed Lambda Calculi and Applications , 2011.

• 53 John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP , 1983.

• 54 John C Reynolds. Preliminary design of the programming language forsythe. Technical report, Carnegie Mellon University, 1988.

• 55 John C. Reynolds. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS) , pages 675–700. Springer Berlin Heidelberg, 1991.

• 56 Chieri Saito and Atsushi Igarashi. Matching ThisType to subtyping. In Symposium on Applied Computing (SAC) , 2009.

• 57 Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Lightweight family polymorphism. Journal of Functional Programming , 18(03), 2007.

• 58 Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P Black. Traits: Composable units of behaviour. In European Conference on Object-Oriented Programming , 2003.

• 59 Jan Schwinghammer. Coherence of subsumption for monadic types. Journal of Functional Programming , 19(02):157, 2008.

• 60 Jeremy Siek, Peter Thiemann, and Philip Wadler. Blame and coercion: together again for the first time. In Conference on Programming Language Design and Implementation , 2015.

• 61 Richard Statman. Logical relations and the typed λ -calculus. Information and Control , 65(2-3):85–97, 1985.

• 62 Rick Statman. A finite model property for intersection types. Electronic Proceedings in Theoretical Computer Science , 177:1–9, 2015.

• 63 W. W. Tait. Intensional interpretations of functionals of finite type i. The Journal of symbolic logic , 32(2):198–212, 1967.

• 64 Philip Wadler. The expression problem. Java-genericity mailing list , 1998.

• 65 Yanlin Wang and Bruno C d S Oliveira. The expression problem, trivially! In Proceedings of the 15th International Conference on Modularity , 2016.

• 66 Yizhou Zhang and Andrew C. Myers. Familia: unifying interfaces, type classes, and family polymorphism. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications , 2017.

--- end of page.page_number=28 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:29

A Some Definitions

▶ Definition 32 (Type translation) .

| Nat | = Nat |⊤| = ⟨⟩ |A → B| = |A| →|B| |A & B| = |A| × |B| |{l : A}| = {l : |A|}

▶ Example 33 (Derivation of other direction of distribution) .

▶ Example 34 (Derivation of contravariant distribution) .

( A 1 → A 2) & ( A 3 → A 2) < : A 1 & A 3 → A 2

B Full Type System of NeColus

ECOOP 2018

--- end of page.page_number=29 ---

22:30 The Essence of Nested Composition

A ∗ B

(Disjointness)

(Context typing I)

--- end of page.page_number=30 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:31

ECOOP 2018

--- end of page.page_number=31 ---

22:32 The Essence of Nested Composition

C Full Type System of λc

c ⊢ τ 1 ▷τ 2 (Coercion typing) cotyp-trans cotyp-refl cotyp-top cotyp-topArr c 1 ⊢ τ 2 ▷τ 3 c 2 ⊢ τ 1 ▷τ 2 id ⊢ τ ▷τ c 1 ◦ c 2 ⊢ τ 1 ▷τ 3 top ⊢ τ ▷ ⟨⟩ top → ⊢⟨⟩ ▷ ⟨⟩→⟨⟩ cotyp-arr cotyp-pair cotyp-topRcd c 1 ⊢ τ 1 [′][▷τ][1] c 2 ⊢ τ 2 ▷τ 2 [′] c 1 ⊢ τ 1 ▷τ 2 c 2 ⊢ τ 1 ▷τ 3 top {l} ⊢⟨⟩ ▷ {l : ⟨⟩} c 1 → c 2 ⊢ τ 1 → τ 2 ▷τ 1 [′][→][τ][ ′] 2 ⟨c 1 , c 2 ⟩⊢ τ 1 ▷τ 2 × τ 3

--- end of page.page_number=32 ---

X. Bi, B. C. d. S. Oliveira, and T. Schrijvers

22:33

cotyp-rcd cotyp-projl cotyp-projr c ⊢ τ 1 ▷τ 2 π 1 ⊢ τ 1 × τ 2 ▷τ 1 π 2 ⊢ τ 1 × τ 2 ▷τ 2 {l : c} ⊢{l : τ 1 } ▷ {l : τ 2 } cotyp-distRcd dist {l} ⊢{l : τ 1 } × {l : τ 2 } ▷ {l : τ 1 × τ 2 } cotyp-distArr

dist → ⊢ ( τ 1 → τ 2) × ( τ 1 → τ 3) ▷τ 1 → τ 2 × τ 3

e −→ e[′] (Small-step reduction) step-id step-trans step-top step-topArr id v −→ v ( c 1 ◦ c 2) v −→ c 1 ( c 2 v ) top v −→⟨⟩ (top → ⟨⟩ ) ⟨⟩−→⟨⟩ step-arr step-topRcd top {l} ⟨⟩−→{l = ⟨⟩} (( c 1 → c 2) v 1) v 2 −→ c 2 ( v 1 ( c 1 v 2)) step-pair step-distArr ⟨c 1 , c 2 ⟩ v −→⟨c 1 v, c 2 v⟩ (dist → ⟨v 1 , v 2 ⟩ ) v 3 −→⟨v 1 v 3 , v 2 v 3 ⟩ step-distRcd step-projl step-projr dist {l} ⟨{l = v 1 }, {l = v 2 }⟩−→{l = ⟨v 1 , v 2 ⟩} π 1 ⟨v 1 , v 2 ⟩−→ v 1 π 2 ⟨v 1 , v 2 ⟩−→ v 2 step-crcd step-beta step-projRcd {l : c} {l = v} −→{l = c v} ( λx. e ) v −→ e [ x �→ v ] {l = v}.l −→ v step-app1 step-app2 step-pair1 step-pair2 e 1 −→ e 1 [′] e 2 −→ e 2 [′] e 1 −→ e 1 [′] e 2 −→ e 2 [′] e 1 e 2 −→ e 1 [′][e][2] v 1 e 2 −→ v 1 e 2 [′] ⟨e 1 , e 2 ⟩−→⟨e 1 [′][,][ e][2] [⟩] ⟨v 1 , e 2 ⟩−→⟨v 1 , e 2 [′][⟩] step-capp step-rcd1 step-rcd2 e −→ e[′] e −→ e[′] e −→ e[′] c e −→ c e[′] {l = e} −→{l = e[′] } e.l −→ e[′] .l

(Small-step reduction)

ECOOP 2018

--- end of page.page_number=33 ---