Distributive Disjoint Polymorphism for Compositional Programming

HKU PL Group Papers - Index

Metadata

• Title: Distributive Disjoint Polymorphism for Compositional Programming
• Venue: ESOP’19
• Area: Merge operator and disjointness
• Source URL: https://i.cs.hku.hk/~bruno/papers/esop2019.pdf
• Downloaded PDF: Distributive-Disjoint-Polymorphism-for-Compositional-Programming.pdf
• Extracted assets: _assets/Distributive-Disjoint-Polymorphism-for-Compositional-Programming/
• Pages: 28
• 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: Distributive Disjoint Polymorphism for Compositional Programming
• line 11: 1 Introduction
• line 35: Distributive Disjoint Polymorphism 3
• line 45: 4 X. Bi et al.
• line 59: 2 Compositional Programming
• line 63: 2.1 A Finally Tagless Encoding in Haskell
• line 71: Distributive Disjoint Polymorphism 5
• line 132: Distributive Disjoint Polymorphism 7
• line 140: 2.2 The SEDEL Encoding
• line 148: As a side note if a new constructor (e.g., rstretch ) is needed, then this is done by means of intersection types ( & creates an intersection type) in SEDEL:
• line 206: Distributive Disjoint Polymorphism 9
• line 229: 3 Semantics of the F[+] i [Calculus]
• line 231: This section gives a formal account of F[+] i[, the first typed calculus combining dis-] joint polymorphism [2] (and disjoint intersection types) with BCD subtyping [3].
• line 246: Fig. 3: Syntax of F[+] i
• line 252: 3.1 Syntax and Semantics
• line 259:
• line 264: Proposition 1 (Type substitution in F i ). If ∆ ⊢ A, ∆ ⊢ B, ( α ∗ C ) ∈ ∆, ∆ ⊢ B ∗ C and well-formed context [ B /α ] ∆, then [ B /α ] ∆ ⊢ [ B /α ] A.
• line 266: Lemma 1 (Type substitution in F[+] i [).] [If][∆][⊢][A,][∆][⊢][B,][(] [α][ ∗][C][)] [∈][∆][and] well-formed context [ B /α ] ∆, then [ B /α ] ∆ ⊢ [ B /α ] A.
• line 270: Distributive Disjoint Polymorphism 11
• line 273:
• line 280: Fig. 4: Declarative subtyping
• line 289:
• line 297:
• line 301:
• line 305:
• line 314: Distributive Disjoint Polymorphism 13
• line 320: |∆⊢A ∗B|||||||||||(Disjointness)|
• line 336: Fig. 6: Selected rules for disjointness
• line 338: 3.2 Disjointness
• line 363: Fig. 7: Syntax of F co
• line 369: 3.3 Elaboration and Type Safety
• line 371: The dynamic semantics of F[+] i is given by elaboration into a target calculus. The target calculus F co is the standard call-by-value System F extended with products and coercions. The syntax of F co is shown in Fig. 7.
• line 386: Distributive Disjoint Polymorphism 15
• line 398: Fig. 8: Selected reduction rules
• line 405:
• line 410: Theorem 1 (Preservation). If • ; • ⊢ e : τ and e −→ e[′] , then • ; • ⊢ e[′] : τ . Theorem 2 (Progress). If • ; • ⊢ e : τ , either e is a value, or ∃e[′] . e −→ e[′] .
• line 418: Lemma 2 (Elaboration soundness). We have that:
• line 426: 4 Algorithmic System and Decidability
• line 432: 4.1 Algorithmic Subtyping Rules
• line 444: For brevity of the algorithm, we use metavariable c to mean type constants:
• line 452: Distributive Disjoint Polymorphism 17
• line 455:
• line 462: Fig. 9: Algorithmic subtyping
• line 464: Correctness of the algorithm. We prove that the algorithm is sound and complete with respect to the specification. We refer the reader to our Coq formalization for more details. We only show the two major theorems:
• line 466: Theorem 3 (Soundness). If Q ⊢ A < : B ⇝ co then A < : Q ⇒ B ⇝ co.
• line 468: Theorem 4 (Completeness). If A < : B ⇝ co, then ∃co[′] . [] ⊢ A < : B ⇝ co[′] .
• line 470: 4.2 Decidability
• line 474: Lemma 3 (Decidability of algorithmic subtyping). Given Q, A and B, it is decidable whether there exists co, such that Q ⊢ A < : B ⇝ co.
• line 476: Lemma 4 (Decidability of disjointness checking). Given ∆, A and B, it is decidable whether ∆ ⊢ A ∗ B.
• line 485:
• line 490: 5 Establishing Coherence for F[+] i
• line 492: i
• line 496: 5.1 The Challenge
• line 502: Distributive Disjoint Polymorphism 19
• line 508: 5.2 Impredicativity and Disjointness at Odds
• line 515:
• line 523:
• line 529:
• line 537:
• line 549:
• line 554: 5.3 The Canonicity Relation for F[+] i
• line 556: i
• line 561:
• line 568: The relation V � A ; B � is defined by induction on the structures of A and B . For integers, it requires the two values to be literally the same. For two records to
• line 572: Distributive Disjoint Polymorphism 21
• line 579:
• line 583:
• line 587:
• line 592: Lemma 5 (Well-foundedness). The canonicity relation of F[+] i[is well-founded.]
• line 596: 5.4 Establishing Coherence
• line 604: Definition 3 (Logical equivalence ⋍ log ).
• line 616: Definition 5 (Contextual Equivalence ⋍ ctx ).
• line 622: Theorem 5 (Coherence). We have that
• line 625:
• line 629:
• line 634: 6 Related Work
• line 640: Distributive Disjoint Polymorphism 23
• line 654: |Disjointness|||||||
• line 655: |Unrestricted intersections|||||||
• line 656: |BCD subtyping|||||||

Full converted paper text

Distributive Disjoint Polymorphism for Compositional Programming

Xuan Bi[1] , Ningning Xie[1] , Bruno C. d. S. Oliveira[1] , and Tom Schrijvers[2]

1 The University of Hong Kong, Hong Kong, China { xbi,nnxie,bruno } @cs.hku.hk

2 KU Leuven, Leuven, Belgium tom.schrijvers@cs.kuleuven.be

Abstract. Popular programming techniques such as shallow embeddings of Domain Specific Languages (DSLs), finally tagless or object algebras are built on the principle of compositionality . However, existing programming languages only support simple compositional designs well, and have limited support for more sophisticated ones. This paper presents the F[+] i[calculus, which supports highly modular and] compositional designs that improve on existing techniques. These improvements are due to the combination of three features: disjoint intersection types with a merge operator ; parametric (disjoint) polymorphism ; and BCD-style distributive subtyping . The main technical challenge is F[+] i[’s][proof][of][coherence.][A][naive][adaptation][of][ideas][used][in][System][F’s] parametricity to canonicity (the logical relation used by F[+] i[to][prove][co-] herence) results in an ill-founded logical relation. To solve the problem our canonicity relation employs a different technique based on immediate substitutions and a restriction to predicative instantiations. Besides coherence, we show several other important meta-theoretical results, such as type-safety, sound and complete algorithmic subtyping, and decidability of the type system. Remarkably, unlike F < :’s bounded polymorphism , disjoint polymorphism in F[+] i[supports][decidable][type-checking.]

1 Introduction

Compositionality is a desirable property in programming designs. Broadly defined, it is the principle that a system should be built by composing smaller subsystems. For instance, in the area of programming languages, compositionality is a key aspect of denotational semantics [48, 49], where the denotation of a program is constructed from the denotations of its parts. Compositional definitions have many benefits. One is ease of reasoning: since compositional definitions are recursively defined over smaller elements they can typically be reasoned about using induction. Another benefit is that compositional definitions are easy to extend, without modifying previous definitions.

Programming techniques that support compositional definitions include: shallow embeddings of Domain Specific Languages (DSLs) [20], finally tagless [11], polymorphic embeddings [26] or object algebras [35]. These techniques allow us

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

2 X. Bi et al.

to create compositional definitions, which are easy to extend without modifications. Moreover, when modeling semantics, both finally tagless and object algebras support multiple interpretations (or denotations) of syntax, thus offering a solution to the well-known Expression Problem [53]. Because of these benefits these techniques have become popular both in the functional and object-oriented programming communities.

However, programming languages often only support simple compositional designs well, while support for more sophisticated compositional designs is lacking. For instance, once we have multiple interpretations of syntax, we may wish to compose them. Particularly useful is a merge combinator, which composes two interpretations [35, 37, 42] to form a new interpretation that, when executed, returns the results of both interpretations.

The merge combinator can be manually defined in existing programming languages, and be used in combination with techniques such as finally tagless or object algebras. Moreover variants of the merge combinator are useful to model more complex combinations of interpretations. A good example are so-called dependent interpretations, where an interpretation does not depend only on itself, but also on a different interpretation. These definitions with dependencies are quite common in practice, and, although they are not orthogonal to the interpretation they depend on, we would like to model them (and also mutually dependent interpretations) in a modular and compositional style.

Defining the merge combinator in existing programming languages is verbose and cumbersome, requiring code for every new kind of syntax. Yet, that code is essentially mechanical and ought to be automated. While using advanced meta-programming techniques enables automating the merge combinator to a large extent in existing programming languages [37, 42], those techniques have several problems: error messages can be problematic, type-unsafe reflection is needed in some approaches [37] and advanced type-level features are required in others [42]. An alternative to the merge combinator that supports modular multiple interpretations and works in OO languages with support for some form of multiple inheritance and covariant type-refinement of fields has also been recently proposed [55]. While this approach is relatively simple, it still requires a lot of manual boilerplate code for composition of interpretations.

This paper presents a calculus and polymorphic type system with (disjoint) intersection types [36], called F[+] i[.][F][+] i supports our broader notion of compositional designs, and enables the development of highly modular and reusable programs. F[+] i[has][a][built-in][merge][operator][and][a][powerful][subtyping][relation] that are used to automate the composition of multiple (possibly dependent) interpretations. In F[+] i subtyping is coercive and enables the automatic generation of coercions in a type-directed fashion. This process is similar to that of other type-directed code generation mechanisms such as type classes [52], which eliminate boilerplate code associated to the dictionary translation [52].

F[+] i[continues a line of research on disjoint intersection types. Previous work on] disjoint polymorphism (the F i calculus) [2] studied the combination of parametric polymorphism and disjoint intersection types, but its subtyping relation does

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

Distributive Disjoint Polymorphism 3

not support BCD-style distributivity rules [3] and the type system also prevents unrestricted intersections [16]. More recently the NeColus calculus (or λ[+] i[)]5 introduced a system with disjoint intersection types and BCD-style distributivity rules, but did not account for parametric polymorphism. F[+] i[is][unique][in][that][it] combines all three features in a single calculus: disjoint intersection types and a merge operator ; parametric (disjoint) polymorphism ; and a BCD-style subtyping relation with distributivity rules . The three features together allow us to improve upon the finally tagless and object algebra approaches and support advanced compositional designs. Moreover previous work on disjoint intersection types has shown various other applications that are also possible in F[+] i[,][including:] first-class traits and dynamic inheritance [4], extensible records and dynamic mixins [2], and nested composition and family polymorphism [5].

Unfortunately the combination of the three features has non-trivial complications. The main technical challenge (like for most other calculi with disjoint intersection types) is the proof of coherence for F[+] i[.][Because][of][the][presence][of] BCD-style distributivity rules, our coherence proof is based on the recent approach employed in λ[+] i [5], which uses a heterogeneous logical relation called canonicity . To account for polymorphism, which λ[+] i[’s][canonicity][does][not][sup-] port, we originally wanted to incorporate the relevant parts of System F’s logical relation [43]. However, due to a mismatch between the two relations, this did not work. The parametricity relation has been carefully set up with a delayed type substitution to avoid ill-foundedness due to its impredicative polymorphism. Unfortunately, canonicity is a heterogeneous relation and needs to account for cases that cannot be expressed with the delayed substitution setup of the homogeneous parametricity relation. Therefore, to handle those heterogeneous cases, we resorted to immediate substitutions and predicative instantiations . We do not believe that predicativity is a severe restriction in practice, since many source languages (e.g., those based on the Hindley-Milner type system like Haskell and OCaml) are themselves predicative and do not require the full generality of an impredicative core language. Should impredicative instantiation be required, we expect that step-indexing [1] can be used to recover well-foundedness, though at the cost of a much more complicated coherence proof.

The formalization and metatheory of F[+] i[are][a][significant][advance][over][that] of F i . Besides the support for distributive subtyping, F[+] i[removes several restric-] tions imposed by the syntactic coherence proof in F i . In particular F[+] i[supports] unrestricted intersections, which are forbidden in F i . Unrestricted intersections enable, for example, encoding certain forms of bounded quantification [39]. Moreover the new proof method is more robust with respect to language extensions. For instance, F[+] i[supports][the][bottom][type][without][significant][complications][in] the proofs, while it was a challenging open problem in F i . A final interesting aspect is that F[+] i[’s][type-checking][is][decidable.][In][the][design][space][of][languages] with polymorphism and subtyping, similar mechanisms have been known to lead to undecidability. Pierce’s seminal paper “ Bounded quantification is undecidable ” [40] shows that the contravariant subtyping rule for bounded quantification in F < : leads to undecidability of subtyping. In F[+] i[the][contravariant][rule]

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

4 X. Bi et al.

for disjoint quantification retains decidability. Since with unrestricted intersections F[+] i[can][express][several][use][cases][of][bounded][quantification,][F][+] i[could][be] an interesting and decidable alternative to F < :.

In summary the contributions of this paper are:

• The F[+] i calculus, which is the first calculus to combine disjoint intersection types, BCD-style distributive subtyping and disjoint polymorphism. We show several meta-theoretical results, such as type-safety , sound and complete algorithmic subtyping , coherence and decidability of the type system. F[+] i[includes][the] [bottom][type][,][which][was][considered][to][be][a][significant][chal-] lenge in previous work on disjoint polymorphism [2].

• An extension of the canonicity relation with polymorphism, which enables the proof of coherence of F[+] i[.][We][show][that][the][ideas][of][System][F’s] parametricity cannot be ported to F[+] i[.][To][overcome][the][problem][we][use][a] technique based on immediate substitutions and a predicativity restriction.

• – Improved compositional designs: We show that F[+] i[’s][combination][of] features enables improved compositional programming designs and supports automated composition of interpretations in programming techniques like object algebras and finally tagless.

• Implementation and proofs: All of the metatheory of this paper, except some manual proofs of decidability, has been mechanically formalized in Coq. Furthermore, F[+] i[is implemented and all code presented in the paper is avail-] able. The implementation, Coq proofs and extended version with appendices can be found in https://github.com/bixuanzju/ESOP2019-artifact .

2 Compositional Programming

To demonstrate the compositional properties of F[+] i[we][use][Gibbons][and][Wu’s] shallow embeddings of parallel prefix circuits [20]. By means of several different shallow embeddings, we first illustrate the short-comings of a state-of-the-art compositional approach, popularly known as a finally tagless encoding [11], in Haskell. Next we show how parametric polymorphism and distributive intersection types provide a more elegant and compact solution in SEDEL [4], a source language built on top of our F[+] i[calculus.]

2.1 A Finally Tagless Encoding in Haskell

The circuit DSL represents networks that map a number of inputs (known as the width) of some type A onto the same number of outputs of the same type. The outputs combine (with repetitions) one or more inputs using a binary associative operator ⊕ : A × A → A . A particularly interesting class of circuits that can be expressed in the DSL are parallel prefix circuits . These represent computations that take n > 0 inputs x 1 , … , xn and produce n outputs y 1 , … , yn , where yi = x 1 ⊕ x 2 ⊕ … ⊕ xi .

The DSL features 5 language primitives: two basic circuit constructors and three circuit combinators. These are captured in the Haskell type class Circuit :

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

Distributive Disjoint Polymorphism 5

data Width = W { width :: Int } data Depth = D { depth :: Int } instance Circuit Width where instance Circuit Depth where identity n = W n identity n = D 0 fan n = W n fan n = D 1 beside c1 c2 = beside c1 c2 = W (width c1 + width c2) D ( max (depth c1) (depth c2)) above c1 c2 = c1 above c1 c2 = D (depth c1 + depth c2) stretch ws c = W ( sum ws) stretch ws c = c

(a) Width embedding (b) Depth embedding

Fig. 1: Two finally tagless embeddings of circuits.

class Circuit c where identity :: Int → c fan :: Int → c beside :: c → c → c above :: c → c → c stretch :: [ Int ] → c → c

An identity circuit with n inputs xi , has n outputs yi = xi . A fan circuit has n inputs xi and n outputs yi , where y 1 = x 1 and yj = x 1 ⊕ xj ( j > 1). The binary beside combinator puts two circuits in parallel; the combined circuit takes the inputs of both circuits to the outputs of both circuits. The binary above combinator connects the outputs of the first circuit to the inputs of the second; the width of both circuits has to be same. Finally, stretch ws c interleaves the wires of circuit c with bundles of additional wires that map their input straight on their output. The ws parameter specifies the width of the consecutive bundles; the i th wire of c is preceded by a bundle of width wsi − 1.

Basic width and depth embeddings. Figure 1 shows two simple shallow embeddings, which represent a circuit respectively in terms of its width and its depth. The former denotes the number of inputs/outputs of a circuit, while the latter is the maximal number of ⊕ operators between any input and output. Both definitions follow the same setup: a new Haskell datatype ( Width / Depth ) wraps the primitive result value and provides an instance of the Circuit type class that interprets the 5 DSL primitives accordingly. The following code creates a so-called Brent-Kung parallel prefix circuit [9]:

e1::Width
e1=above(beside(fan2)(fan2))
(above(stretch[2,2](fan2))

(beside(beside(identity1)(fan2))(identity1)))

Here e1 evaluates to W {width = 4} . If we want to know the depth of the circuit, we have to change type signature to Depth .

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

6 X. Bi et al.

Interpreting multiple ways. Fortunately, with the help of polymorphism we can define a type of circuits that support multiple interpretations at once.

type DCircuit = forall c. Circuit c ⇒ c

This way we can provide a single Brent-Kung parallel prefix circuit definition that can be reused for different interpretations.

brentKung::DCircuit
brentKung=above(beside(fan2)(fan2))
(above(stretch[2,2](fan2))
(beside(beside(identity1)(fan2))(identity1)))

A type annotation then selects the desired interpretation. For instance, brentKung :: Width yields the width and brentKung :: Depth the depth.

Composition of embeddings. What is not ideal in the above code is that the same brentKung circuit is processed twice, if we want to execute both interpretations. We can do better by processing the circuit only once, computing both interpretations simultaneously. The finally tagless encoding achieves this with a boilerplate instance for tuples of interpretations.

instance (Circuit c1, Circuit c2) ⇒ Circuit (c1, c2) where identity n = (identity n, identity n) fan n = (fan n, fan n) beside c1 c2 = (beside ( fst c1) ( fst c2), beside ( snd c1) ( snd c2)) above c1 c2 = (above ( fst c1) ( fst c2), above ( snd c1) ( snd c2)) stretch ws c = (stretch ws ( fst c), stretch ws ( snd c))

Now we can get both embeddings simultaneously as follows:

e12 :: (Width, Depth) e12 = brentKung This evaluates to (W {width = 4}, D {depth = 2}) .

Composition of dependent interpretations. The composition above is easy because the two embeddings are orthogonal. In contrast, the composition of dependent interpretations is rather cumbersome in the standard finally tagless setup. An example of the latter is the interpretation of circuits as their well-sizedness, which captures whether circuits are well-formed. This interpretation depends on the interpretation of circuits as their width.[3]

data WellSized = WS { wS :: Bool , ox :: Width } instance Circuit WellSized where identity n = WS True (identity n) fan n = WS True (fan n) beside c1 c2 = WS (wS c1 && wS c2) (beside (ox c1) (ox c2))

3 Dependent recursion schemes are also known as zygomorphism [18] after the ancient Greek word ζυγ ο ν for yoke. We have labeled the Width field with ox because it is pulling the yoke.

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

Distributive Disjoint Polymorphism 7

above c1 c2 = WS (wS c1 && wS c2 && width (ox c1) == width (ox c2)) (above (ox c1) (ox c2)) stretch ws c = WS (wS c && length ws==width (ox c)) (stretch ws (ox c))

The WellSized datatype represents the well-sizedness of a circuit with a Boolean, and also keeps track of the circuit’s width. The 5 primitives compute the wellsizedness in terms of both the width and well-sizedness of the subcomponents. What makes the code cumbersome is that it has to explicitly delegate to the Width interpretation to collect this additional information.

With the help of a substantially more complicated setup that features a dozen Haskell language extensions, and advanced programming techniques, we can make the explicit delegation implicit (see the appendix). Nevertheless, that approach still requires a lot of boilerplate that needs to be repeated for each DSL, as well as explicit projections that need to be written in each interpretation. Another alternative Haskell encoding that also enables multiple dependent interpretations is proposed by Zhang and Oliveira [55], but it does not eliminate the explicit delegation and still requires substantial amounts of boilerplate. A final remark is that adding new primitives (e.g., a “right stretch” rstretch combinator [25]) can also be easily achieved [46].

2.2 The SEDEL Encoding

SEDEL is a source language that elaborates to F[+] i[,][adding][a][few][convenient] source level constructs. The SEDEL setup of the circuit DSL is similar to the finally tagless approach. Instead of a Circuit c type class, there is a Circuit[C] type that gathers the 5 circuit primitives in a record. Like in Haskell, the type parameter C expresses that the interpretation of circuits is a parameter.

type Circuit[C] = {

identity : Int → C, fan : Int → C, beside : C → C → C, above : C → C → C, stretch : List[Int] → C → C };

As a side note if a new constructor (e.g., rstretch ) is needed, then this is done by means of intersection types ( & creates an intersection type) in SEDEL:

type NCircuit[C] = Circuit[C] & { rstretch : List[Int] → C → C };

Figure 2 shows the two basic shallow embeddings for width and depth. In both cases, a named SEDEL definition replaces the corresponding unnamed Haskell type class instance in providing the implementations of the 5 language primitives for a particular interpretation.

The use of the SEDEL embeddings is different from that of their Haskell counterparts. Where Haskell implicitly selects the appropriate type class instance based on the available type information, in SEDEL the programmer explicitly selects the implementation following the style used by object algebras. The following code does this by building a circuit with l1 (short for language1 ).

l1=language1;

e1=l1.above(l1.beside(l1.fan2)(l1.fan2))

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

8 X. Bi et al.

type Width = { width : Int }; language1 : Circuit[Width] = { identity (n : Int) = { width = n }, fan (n : Int) = { width = n }, beside (c1 : Width) (c2 : Width) = { width = c1.width + c2.width }, above (c1 : Width) (c2 : Width) = { width = c1.width }, stretch (ws : List[Int]) (c : Width) = { width = sum ws } }; type Depth = { depth : Int }; language2 : Circuit[Depth] = { identity (n : Int) = { depth = 0 }, fan (n : Int) = { depth = 1 }, beside (c1 : Depth) (c2 : Depth) = { depth = max c1.depth c2.depth}, above (c1 : Depth) (c2 : Depth) = { depth = c1.depth + c2.depth}, stretch (ws : List[Int]) (c : Depth) = { depth = c.depth } };

Fig. 2: Two SEDEL embeddings of circuits.

(l1.above(l1.stretch(cons2(cons2nil))(l1.fan2))

(l1.beside(l1.beside(l1.identity1)(l1.fan2))(l1.identity1)));

Here e1 evaluates to {width = 4} . If we want to know the depth of the circuit, we have to replicate the code with language2 .

Dynamically reusable circuits. Just like in Haskell, we can use polymorphism to define a type of circuits that can be interpreted with different languages.

type DCircuit = { accept : forall C. Circuit[C] → C };

In contrast to the Haskell solution, this implementation explicitly accepts the implementation.

brentKung:DCircuit={
acceptCl=l.above(l.beside(l.fan2)(l.fan2))
(l.above(l.stretch(cons2(cons2nil))(l.fan2))
(l.beside(l.beside(l.identity1)(l.fan2))(l.identity1)))};
e1=brentKung.acceptWidthlanguage1;
e2=brentKung.acceptDepthlanguage2;

Automatic composition of languages. Of course, like in Haskell we can also compute both results simultaneously. However, unlike in Haskell, the composition of the two interpretation requires no boilerplate whatsoever—in particular, there is no SEDEL counterpart of the Circuit (c1, c2) instance. Instead, we can just compose the two interpretations with the term-level merge operator ( ,, ) and specify the desired type Circuit[Width & Depth] .

language3:Circuit[Width&Depth]=language1,,language2;
e3=brentKung.accept(Width&Depth)language3;

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

Distributive Disjoint Polymorphism 9

Here the use of the merge operator creates a term with the intersection type Circuit[Width] & Circuit[Depth] . Implicitly, the SEDEL type system takes care of the details, turning this intersection type into Circuit[Width & Depth] . This is possible because intersection ( & ) distributes over function and record types (a distinctive feature of BCD-style subtyping).

Composition of dependent interpretations. In SEDEL the composition scales nicely to dependent interpretations. For instance, the well-sizedness interpretation can be expressed without explicit projections.

type WellSized = { wS : Bool }; language4 = { identity (n : Int) = { wS = true }, fan (n : Int) = { wS = true }, above (c1 : WellSized & Width) (c2 : WellSized & Width) = { wS = c1.wS && c2.wS && c1.width == c2.width }, beside (c1 : WellSized) (c2 : WellSized) = { wS = c1.wS && c2.wS }, stretch (ws : List[Int]) (c : WellSized & Width) = { wS = c.wS && length ws == c.width } };

Here the WellSized & Width type in the above and stretch cases expresses that both the well-sizedness and width of subcircuits must be given, and that the width implementation is left as a dependency—when language4 is used, then the width implementation must be provided. Again, the distributive properties of & in the type system take care of merging the two interpretations.

e4=brentKung.accept(WellSized&Width)(language1,,language4);
main=e4.wS--Output:true

Disjoint polymorphism and dynamic merges. While it may seem from the above examples that definitions have to be merged statically, SEDEL in fact supports dynamic merges. For instance, we can encapsulate the merge operator in the combine function while abstracting over the two components x and y that are merged as well as over their types A and B .

combineA[B*A](x:A)(y:B)=x,,y;

This way the components x and y are only known at runtime and thus the merge can only happen at that time. The types A and B cannot be chosen entirely freely. For instance, if both components would contribute an implementation for the same method, which implementation is provided by the combination would be ambiguous. To avoid this problem the two types A and B have to be disjoint . This is expressed in the disjointness constraint * A on the quantifier of the type variable B . If a quantifier mentions no disjointness constraint, like that of A , it defaults to the trivial * ⊤ constraint which implies no restriction.

3 Semantics of the F[+] i [Calculus]

This section gives a formal account of F[+] i[, the first typed calculus combining dis-] joint polymorphism [2] (and disjoint intersection types) with BCD subtyping [3].

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

10 X. Bi et al.

|Types|A, B, |C ::=|Int| ⊤| ⊥| A →B | A&B | {l :A} | α | ∀(α ∗A). B| |---|---|---|---| |Expressions|E|::=|x | i | ⊤| λx. E | E_1_E_2 | E_1, , E_2 | E :A | {l =E} | E.l| |||||Λ(α ∗A). E | E A_| |Term contexts|Γ|::=|• | Γ, x :A| |Type contexts|∆|::=|• | ∆, α ∗A|

Fig. 3: Syntax of F[+] i

i

The main differences to F i are in the subtyping, well-formedness and disjointness relations. F[+] i[adds BCD subtyping and unrestricted intersections, and also closes] an open problem of F i by including the bottom type. The dynamic semantics of F[+] i[is][given][by][elaboration][to][the][target][calculus][F] [co][—a][variant][of][System][F] extended with products and explicit coercions.

3.1 Syntax and Semantics

Figure 3 shows the syntax of F[+] i[. Metavariables] [ A][,][ B][,][ C][range over types. Types] include standard constructs from prior work [2, 36]: integers Int, the top type ⊤ , arrows A → B , intersections A & B , single-field record types {l : A} and disjoint quantification ∀ ( α ∗ A ) . B . One novelty in F[+] i[is][the][addition][of][the][uninhabited] bottom type ⊥ . Metavariable E ranges over expressions. Expressions are integer literals i , the top value ⊤ , lambda abstractions λx . E , applications E 1 E 2, merges E 1 , , E 2, annotated terms E : A , single-field records {l = E } , record projections E .l , type abstractions Λ ( α ∗ A ) . E and type applications E A .

Well-formedness and unrestricted intersections. F[+] i[’s][well-formedness][judgment] of types ∆ ⊢ A is standard, and only enforces well-scoping. This is one of the key differences from F i , which uses well-formedness to also ensure that all intersection types are disjoint. In other words, while in F i all valid intersection types must be disjoint, in F[+] i[unrestricted][intersection][types][such][as][Int][ &][ Int][are][allowed.] More specifically, the well-formedness of intersection types in F[+] i[and][F] [i][is:]

Notice that F i has an extra disjointness condition ∆ ⊢ A ∗ B in the premise. This is crucial for F i ’s syntactic method for proving coherence, but also burdens the calculus with various syntactic restrictions and complicates its metatheory. For example, it requires extra effort to show that F i only produces disjoint intersection types. As a consequence, F i features a weaker substitution lemma (note the gray part in Proposition 1) than F[+] i[(Lemma][1).]

Proposition 1 (Type substitution in F i ). If ∆ ⊢ A, ∆ ⊢ B, ( α ∗ C ) ∈ ∆, ∆ ⊢ B ∗ C and well-formed context [ B /α ] ∆, then [ B /α ] ∆ ⊢ [ B /α ] A.

Lemma 1 (Type substitution in F[+] i [).] [If][∆][⊢][A,][∆][⊢][B,][(] [α][ ∗][C][)] [∈][∆][and] well-formed context [ B /α ] ∆, then [ B /α ] ∆ ⊢ [ B /α ] A.

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

Distributive Disjoint Polymorphism 11

----- Start of picture text -----
A < : B ⇝ co (Declarative subtyping)
S-trans
S-refl S-top
A 2 < : A 3 ⇝ co 1 A 1 < : A 2 ⇝ co 2
A < : A ⇝ id A 1 < : A 3 ⇝ co 1 ◦ co 2 A < : ⊤ ⇝ top
S-rcd
S-andl S-andr
A < : B ⇝ co
{l : A} < : {l : B } ⇝ co A 1 & A 2 < : A 1 ⇝ π 1 A 1 & A 2 < : A 2 ⇝ π 2
S-and
S-arr
B 1 < : A 1 ⇝ co 1 A 2 < : B 2 ⇝ co 2 A 1 < : A 2 ⇝ co 1 A 1 < : A 3 ⇝ co 2
A 1 → A 2 < : B 1 → B 2 ⇝ co 1 → co 2 A 1 < : A 2 & A 3 ⇝ ⟨co 1 , co 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 S-bot
{l : A} & {l : B } < : {l : A & B } ⇝ id ⊤ < : {l : ⊤} ⇝ id ⊥ < : A ⇝ bot
S-forall
S-topAll
B 1 < : B 2 ⇝ co A 2 < : A 1
∀ ( α ∗ A 1) . B 1 < : ∀ ( α ∗ A 2) . B 2 ⇝ co∀ ⊤ < : ∀ ( α ∗⊤ ) . ⊤ ⇝ top ∀
S-distAll
( ∀ ( α ∗ A ) . B 1) & ( ∀ ( α ∗ A ) . B 2) < : ∀ ( α ∗ A ) . B 1 & B 2 ⇝ dist ∀
----- End of picture text -----

Fig. 4: Declarative subtyping

Declarative subtyping. F[+] i[’s][subtyping][judgment][is][another][major][difference][to] F i , because it features BCD-style subtyping and a rule for the bottom type. The full set of subtyping rules are shown in Fig. 4. The reader is advised to ignore the gray parts for now. Our subtyping rules extend the BCD-style subtyping rules from λ[+] i[[5] with a rule for parametric (disjoint) polymorphism (rule][ S-forall][).] Moreover, we have three new rules: rule S-bot for the bottom type, and rules S- distAll and S-topAll for distributivity of disjoint quantification. The subtyping relation is a partial order (rules S-refl and S-trans). Most of the rules are quite standard. ⊥ is a subtype of all types (rule S-bot). Subtyping of disjoint quantification is covariant in its body, and contravariant in its disjointness constraints (rule S-forall). Of particular interest are those so-called “distributivity” rules: rule S-distArr says intersections distribute over arrows; rule S- distRcd says intersections distribute over records. Similarly, rule S-distAll dictates that intersections may distribute over disjoint quantifiers.

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

12 X. Bi et al.

----- Start of picture text -----
∆ ; Γ ⊢ E ⇒ A ⇝ e (Inference)
T-top T-nat T-var
⊢ ∆ ∆ ⊢ Γ ⊢ ∆ ∆ ⊢ Γ ⊢ ∆ ∆ ⊢ Γ ( x : A ) ∈ Γ
∆ ; Γ ⊢⊤⇒⊤ ⇝ ⟨⟩ ∆ ; Γ ⊢ i ⇒ Int ⇝ i ∆ ; Γ ⊢ x ⇒ A ⇝ x
T-merge
T-app
∆ ; Γ ⊢ E 1 ⇒ A 1 → A 2 ⇝ e 1 ∆ ; Γ ⊢ E 1 ⇒ A 1 ⇝ e 1
∆ ; Γ ⊢ E 2 ⇐ A 1 ⇝ e 2 ∆ ; Γ ⊢ E 2 ⇒ A 2 ⇝ e 2 ∆ ⊢ A 1 ∗ A 2
∆ ; Γ ⊢ E 1 E 2 ⇒ A 2 ⇝ e 1 e 2 ∆ ; Γ ⊢ E 1 , , E 2 ⇒ A 1 & A 2 ⇝ ⟨e 1 , e 2 ⟩
T-anno T-rcd
∆ ; Γ ⊢ E ⇐ A ⇝ e ∆ ; Γ ⊢ E ⇒ A ⇝ e
∆ ; Γ ⊢ E : A ⇒ A ⇝ e ∆ ; Γ ⊢{l = E } ⇒{l : A} ⇝ e
T-proj T-tabs
∆ ; Γ ⊢ E ⇒{l : A} ⇝ e ∆, α ∗ A ; Γ ⊢ E ⇒ B ⇝ e ∆ ⊢ A ∆ ⊢ Γ
∆ ; Γ ⊢ E .l ⇒ A ⇝ e ∆ ; Γ ⊢ Λ ( α ∗ A ) . E ⇒∀ ( α ∗ A ) . B ⇝ Λα. e
T-tapp
∆ ; Γ ⊢ E ⇒∀ ( α ∗ B ) . C ⇝ e ∆ ⊢ A ∗ B
∆ ; Γ ⊢ E A ⇒ [ A/α ] C ⇝ e |A|
----- End of picture text -----

Fig. 5: Bidirectional type system

Typing rules. F[+] i features a bidirectional type system inherited from F i . The full set of typing rules are shown in Fig. 5. Again we ignore the gray parts and explain them in Section 3.3. The inference judgment ∆ ; Γ ⊢ E ⇒ A says that we can synthesize the type A under the contexts ∆ and Γ . The checking judgment ∆ ; Γ ⊢ E ⇐ A asserts that E checks against the type A under the contexts ∆ and Γ . Most of the rules are quite standard in the literature. The merge expression E 1 , , E 2 is well-typed if both sub-expressions are well-typed, and their types are disjoint (rule T-merge). The disjointness relation will be explained in Section 3.2. To infer a type abstraction (rule T-tabs), we add disjointness constraints to the type context. For a type application (rule T- tapp), we check that the type argument satisfies the disjointness constraints. Rules T-merge and T-tapp are the only rules checking disjointness.

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

Distributive Disjoint Polymorphism 13

⌉A⌈											(Top-like types)
TL-top		TL-and ⌉A⌈		⌉B⌈			TL-arr ⌉B⌈		TL-rcd ⌉A⌈	TL-all ⌉B⌈
⌉⊤⌈			⌉A&B⌈				⌉A →B⌈		⌉{l :A}⌈	⌉∀(α ∗A). B⌈
∆⊢A ∗B											(Disjointness)
	D-topL				D-topR			D-arr
	⌉A⌈						⌉B⌈		_∆⊢A_2_∗B_2
	∆⊢A ∗B					∆⊢A ∗B		_∆⊢A_1 _→A_2_∗B_1			_→B_2
	D-andL							D-andR
	_∆⊢A_1	∗B		∆⊢A_2_∗B				_∆⊢A ∗B_1		_∆⊢A ∗B_2
	_∆⊢A_1&_A_2				∗B				_∆⊢A ∗B_1&_B_2
D-rcdEq					D-rcdNeq				D-tvarL
	∆⊢A ∗B						_l_1 =_l_2		(α ∗A)∈∆ A <:B
∆⊢{l :A} ∗{l :			B}		_∆⊢{l_1 :_A} ∗{l_2			:B}		∆⊢α ∗B
D-tvarR							D-forall				D-ax
(α ∗A)∈∆		A <:B					_∆, α ∗A_1&_A_2		_⊢B_1_∗B_2		A ∗ax B
	∆⊢B ∗α						∆⊢∀(α ∗A_1). B_1_∗∀_(α ∗A_2). _			_B_2	∆⊢A ∗B

Fig. 6: Selected rules for disjointness

3.2 Disjointness

We now turn to another core judgment of F[+] i[—the][disjointness][relation,][shown] in Fig. 6. The disjointness rules are mostly inherited from F i [2], but the new bottom type requires a notable change regarding disjointness with top-like types .

Top-like types. Top-like types are all types that are isomorphic to ⊤ (i.e., simultaneously sub- and supertypes of ⊤ ). Hence, they are inhabited by a single value, isomorphic to the ⊤ value. Fig. 6 captures this notion in a syntax-directed fashion in the ⌉A⌈ predicate. As a historical note, the concept of top-like types was already known by Barendregt et al. [3]. The λi calculus [36] re-discovered it and coined the term “top-like types”; the F i calculus [2] extended it with universal quantifiers. Note that in both calculi, top-like types are solely employed for enabling a syntactic method of proving coherence, and due to the lack of BCD subtyping, they do not have a type-theoretic interpretation of top-like types.

Disjointness rules. The disjointness judgment ∆ ⊢ A ∗ B is helpful to check whether the merge of two expressions of type A and B preserves coherence. Incoherence arises when both expressions produce distinct values for the same

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

14 X. Bi et al.

|Types|τ|::=|Int_| ⟨⟩| τ_1 →τ_2 | τ_1_× τ_2 | α | ∀α. τ| |---|---|---|---| |Terms|e|::=|x | i | ⟨⟩| λx. e | e_1_e_2 | ⟨e_1, e_2⟩| Λα. e | e τ | co e| |Coercions|co|::=|id| co_1_◦co_2 |top|bot| co_1 →co_2 | ⟨co_1, co_2⟩| π_1 | π_2| |||||co∀|dist_→|top_→|top_∀|dist_∀| |Values|v|::=|i | ⟨⟩| λx. e | ⟨v_1, v_2⟩| Λα. e |(co_1 →co_2)v | co∀v| |||||dist_→v |top_→v |top_∀v |dist_∀v| |Term contexts|Ψ|::=|• | Ψ, x :τ| |Type contexts|Φ|::=|• | Φ, α| |Evaluation contexts|E|::=|[·]| E e | v E | ⟨E, e⟩| ⟨v, E⟩| co E | E τ|

Fig. 7: Syntax of F co

type, either directly when they are both of that same type, or through implicit upcasting to a common supertype. Of course we can safely disregard top-like types in this matter because they do not have two distinct values. In short, it suffices to check that the two types have only top-like supertypes in common.

Because ⊥ and any another type A always have A as a common supertype, it follows that ⊥ is only disjoint to A when A is top-like. More generally, if A is a top-like type, then A is disjoint to any type. This is the rationale behind the two rules D-topL and D-topR, which generalize and subsume ∆ ⊢⊤∗ A and ∆ ⊢ A ∗⊤ from F i , and also cater to the bottom type. Two other interesting rules are D-tvarL and D-tvarR, which dictate that a type variable α is disjoint with some type B if its disjointness constraints A is a subtype of B . Disjointness axioms A∗axB (appearing in rule D-ax) take care of two types with different type constructors (e.g., Int and records). Axiom rules can be found in the appendix. Finally we note that the disjointness relation is symmetric.

3.3 Elaboration and Type Safety

The dynamic semantics of F[+] i is given by elaboration into a target calculus. The target calculus F co is the standard call-by-value System F extended with products and coercions. The syntax of F co is shown in Fig. 7.

Type translation. Definition 1 defines the type translation function | · | from F[+] i types A to F co types τ . Most cases are straightforward. For example, ⊥ is mapped to an uninhabited type ∀α. α ; disjoint quantification is mapped to universal quantification, dropping the disjointness constraints. | · | is naturally extended to work on contexts as well.

Definition 1. Type translation | · | is defined as follows:

||Int|=Int||⊤|=⟨⟩||A →B|=|A| →|B|| |---|---|---| ||A&B|=|A| × |B|||{l :A}|=|A|||α|=α| ||⊥|=∀α. α||∀(α ∗A). B|=∀α. |B|||

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

Distributive Disjoint Polymorphism 15

e −→e′				(Single-step reduction)
r-forall		r-topAll	r-distAll
(co∀v)τ −→co(v τ)		(top_∀⟨⟩_)τ −→⟨⟩	(dist_∀⟨v_1_, _	v_2⟩_)τ −→⟨v_1_τ, v_2_τ⟩
				r-ctxt
r-tapp		r-app		e −→e′
(Λα. e)τ −→[τ/α]e		(λx. e)v −→[v/x]e		E[e]−→E[e′]

Fig. 8: Selected reduction rules

Coercions and coercive subtyping. We follow prior work [5, 6] by having a syntactic category for coercions [22]. In Fig. 7, we have several new coercions: bot, co∀ , dist ∀ and top ∀ due to the addition of polymorphism and bottom type. As seen in Fig. 4 the coercive subtyping judgment has the form A < : B ⇝ co , which says that the subtyping derivation for A < : B produces a coercion co that converts terms of type |A| to |B | .

F co static semantics. The typing rules of F co are quite standard. We have one rule t-capp regarding coercion application, which uses the judgment co :: τ ▷τ[′] to type coercions. We show two representative rules ct-forall and ct-bot.

F co dynamic semantics. The dynamic semantics of F co is mostly unremarkable. We write e −→ e[′] to mean one-step reduction. Figure 8 shows selected reduction rules. The first line shows three representative rules regarding coercion reductions. They do not contribute to computation but merely rearrange coercions. Our coercion reduction rules are quite standard but not efficient in terms of space. Nevertheless, there is existing work on space-efficient coercions [23, 50], which should be applicable to our work as well. Rule r-app is the usual β -rule that performs actual computation, and rule r-ctxt handles reduction under an evaluation context. As usual, −→[∗] is the reflexive, transitive closure of −→ . Now we can show that F co is type safe:

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

Elaboration. Now consider the translation parts in Fig. 5. The key idea of the translation follows the prior work [2, 5, 16, 36]: merges are elaborated to pairs (rule T-merge); disjoint quantification and disjoint type applications (rules T- tabs and T-tapp) are elaborated to regular universal quantification and type applications, respectively. Finally, the following lemma connects F[+] i[to][F] [co][:]

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

16 X. Bi et al.

Lemma 2 (Elaboration soundness). We have that:

• If A < : B ⇝ co, then co :: |A| ▷ |B |.

• If ∆ ; Γ ⊢ E ⇒ A ⇝ e, then |∆| ; |Γ | ⊢ e : |A|.

• – If ∆ ; Γ ⊢ E ⇐ A ⇝ e, then |∆| ; |Γ | ⊢ e : |A|.

4 Algorithmic System and Decidability

The subtyping relation in Fig. 4 is highly non-algorithmic due to the presence of a transitivity rule. This section presents an alternative algorithmic formulation. Our algorithm extends that of λ[+] i[,][which][itself][was][inspired][by][Pierce’s][decision] procedure [38], to handle disjoint quantifiers and the bottom type. We then prove that the algorithm is sound and complete with respect to declarative subtyping.

Additionally we prove that the subtyping and disjointness relations are decidable. Although the proofs of this fact are fairly straightforward, it is nonetheless remarkable since it contrasts with the subtyping relation for (full) F < : [10], which is undecidable [40]. Thus while bounded quantification is infamous for its undecidability, disjoint quantification has the nicer property of being decidable.

4.1 Algorithmic Subtyping Rules

While Fig. 4 is a fine specification of how subtyping should behave, it cannot be read directly as a subtyping algorithm for two reasons: (1) the conclusions of rules S-refl and S-trans overlap with the other rules, and (2) the premises of rule S-trans mention a type that does not appear in the conclusion. Simply dropping the two offending rules from the system is not possible without losing expressivity [29]. Thus we need a different approach. Following λ[+] i[,][we][intend] the algorithmic judgment Q ⊢ A < : B to be equivalent to A < : Q ⇒ B , where Q is a queue used to track record labels, domain types and disjointness constraints. The full rules of the algorithmic subtyping of F[+] i[are][shown][Fig.][9.]

Definition 2 ( Q ::= [] | l , Q | B , Q | α ∗ B , Q ). Q ⇒ A is defined as follows:

[]⇒A = A		(B, Q)⇒A = B →(Q ⇒A)
(l, Q)⇒A = {l	:Q ⇒A}	(α ∗B, Q)⇒A = ∀(α ∗B). Q ⇒A

For brevity of the algorithm, we use metavariable c to mean type constants:

Type Constants c ::= Int | ⊥| α

The basic idea of Q ⊢ A < : B is to perform a case analysis on B until it reaches type constants. We explain new rules regarding disjoint quantification and the bottom type. When a quantifier is encountered in B , rule A-forall pushes the type variables with its disjointness constraints onto Q and continue with the body. Correspondingly, in rule A-allConst, when a quantifier is encountered in A , and the head of Q is a type variable, this variable is popped out and we continue with the body. Rule A-bot is similar to its declarative counterpart. Two meta-functions � Q � [⊤] and � Q �[&] are meant to generate correct forms of coercions, and their definitions are shown in the appendix. For other algorithmic rules, we refer to λ[+] i5[for][detailed][explanations.]

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

Distributive Disjoint Polymorphism 17

----- Start of picture text -----
Q ⊢ A < : B ⇝ co (Algorithmic subtyping)
A-and
A-top Q ⊢ A < : B 1 ⇝ co 1 Q ⊢ A < : B 2 ⇝ co 2
Q ⊢ A < : ⊤ ⇝ � Q � [⊤] ◦ top Q ⊢ A < : B 1 & B 2 ⇝ � Q � [&] ◦⟨co 1 , co 2 ⟩
A-arr A-rcd
Q, B 1 ⊢ A < : B 2 ⇝ co Q, l ⊢ A < : B ⇝ co
Q ⊢ A < : B 1 → B 2 ⇝ co Q ⊢ A < : {l : B } ⇝ co
A-forall
A-const A-bot
Q, α ∗ B 1 ⊢ A < : B 2 ⇝ co
Q ⊢ A < : ∀ ( α ∗ B 1) . B 2 ⇝ co [] ⊢ c < : c ⇝ id Q ⊢⊥ < : c ⇝ bot
A-arrConst A-rcdConst
[] ⊢ A < : A 1 ⇝ co 1 Q ⊢ A 2 < : c ⇝ co 2 Q ⊢ A < : c ⇝ co
A, Q ⊢ A 1 → A 2 < : c ⇝ co 1 → co 2 l , Q ⊢{l : A} < : c ⇝ co
A-andConst A-allConst
Q ⊢ Ai < : c ⇝ co i ∈{ 1 , 2 } [] ⊢ A < : A 1 Q ⊢ A 2 < : c ⇝ co
Q ⊢ A 1 & A 2 < : c ⇝ co ◦ πi ( α ∗ A, Q ) ⊢∀ ( α ∗ A 1) . A 2 < : c ⇝ co∀
----- End of picture text -----

Fig. 9: Algorithmic subtyping

Correctness of the algorithm. We prove that the algorithm is sound and complete with respect to the specification. We refer the reader to our Coq formalization for more details. We only show the two major theorems:

Theorem 3 (Soundness). If Q ⊢ A < : B ⇝ co then A < : Q ⇒ B ⇝ co.

Theorem 4 (Completeness). If A < : B ⇝ co, then ∃co[′] . [] ⊢ A < : B ⇝ co[′] .

4.2 Decidability

Moreover, we prove that our algorithmic type system is decidable. To see this, first notice that the bidirectional type system is syntax-directed, so we only need to show decidability of algorithmic subtyping and disjointness. The full (manual) proofs for decidability can be found in the appendix.

Lemma 3 (Decidability of algorithmic subtyping). Given Q, A and B, it is decidable whether there exists co, such that Q ⊢ A < : B ⇝ co.

Lemma 4 (Decidability of disjointness checking). Given ∆, A and B, it is decidable whether ∆ ⊢ A ∗ B.

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

18 X. Bi et al.

One interesting observation here is that although our disjointness quantification has a similar shape to bounded quantification ∀ ( α < : A ) . B in F < : [10], subtyping for F < : is undecidable [40]. In F < :, the subtyping relation between bounded quantification is:

Compared with rule S-forall, both rules are contravariant on bounded/disjoint types, and covariant on the body. However, with bounded quantification it is fundamental to track the bounds in the environment, which complicates the design of the rules and makes subtyping undecidable with rule fsub-forall. Decidability can be recovered by employing an invariant rule for bounded quantification (that is by forcing A 1 and A 2 to be identical). Disjoint quantification does not require such invariant rule for decidability.

5 Establishing Coherence for F[+] i

i

In this section, we establish the coherence property for F[+] i[.][The][proof][strategy] mostly follows that of λ[+] i[,][but][the][construction][of][the][heterogeneous][logical][re-] lation is significantly more complicated. Firstly in Section 5.1 we discuss why adding BCD subtyping to disjoint polymorphism introduces significant complications. In Section 5.2, we discuss why a natural extension of System F’s logical relation to deal with disjoint polymorphism fails. The technical difficulty is well-foundedness , stemming from the interaction between impredicativity and disjointness. Finally in Section 5.3, we present our (predicative) logical relation that is specially crafted to prove coherence for F[+] i[.]

5.1 The Challenge

Before we tackle the coherence of F[+] i[, let us first consider how][ F] [i][(and its prede-] cessor λi ) enforces coherence. Its essentially syntactic approach is to make sure that there is at most one subtyping derivation for any two types. As an immediate consequence, the produced coercions are uniquely determined and thus the calculus is clearly coherent. Key to this approach is the invariant that the type system only produces disjoint intersection types. As we mentioned in Section 3, this invariant complicates the calculus and its metatheory, and leads to a weaker substitution lemma. Moreover, the syntactic coherence approach is incompatible with BCD subtyping, which leads to multiple subtyping derivations with different coercions and requires a more general substitution lemma. To accommodate BCD into λi , Bi et al. [5] have created the λ[+] i[calculus][and][developed][a] semantically-founded proof method based on logical relations. Because λ[+] i[does] not feature polymorphism, the problem at hand is to incorporate support for polymorphism in this semantic approach to coherence, which turns out to be more challenging than is apparent.

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

Distributive Disjoint Polymorphism 19

( v 1 , v 2) ∈V �Int; Int� ≜ ∃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[�] ( ⟨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�

Fig. 10: Selected cases from λ[+] i[’s][canonicity][relation]

5.2 Impredicativity and Disjointness at Odds

Figure 10 shows selected cases of canonicity , which is λ[+] i[’s (heterogeneous) logical] relation used in the coherence proof. The definition captures that two values v 1 and v 2 of types τ 1 and τ 2 are in V � τ 1; τ 2� iff either the types are disjoint or the types are equal and the values are semantically equivalent. Because both alternatives entail coherence, canonicity is key to λ[+] i[’s][coherence][proof.]

Well-foundedness issues. For F[+] i[,][we][need][to][extend][canonicity][with][additional] cases to account for universally quantified types. For reasons that will become clear in Section 5.3, the type indices become source types (rather than target types as in Fig. 10). A naive formulation of one case rule is:

This case is problematic because it destroys the well-foundedness of λ[+] i[’s][logical] relation, which is based on structural induction on the type indices. Indeed, the type [ C 1 /α ] B 1 may well be larger than ∀ ( α ∗ A 1) . B 1.

However, System F’s well-known parametricity logical relation [43] provides us with a means to avoid this problem. Rather than performing the type substitution immediately as in the above rule, we can defer it to a later point by adding it to an extra parameter ρ of the relation, which accumulates the deferred substitutions. This yields a modified rule where the type indices in the recursive occurrences are indeed smaller:

Of course, the deferred substitution has to be performed eventually, to be precise when the type indices are type variables.

Unfortunately, this way we have not only moved the type substitution to the type variable case, but also the ill-foundedness problem. Indeed, this problem is also present in System F. The standard solution is to not fix the relation R by which values at type α are related to V � ρ 1( α ); ρ 2( α )�, but instead to make it a parameter that is tracked by ρ . This yields the following two rules for disjoint quantification and type variables:

( v 1 , v 2) ∈V � ∀ ( α ∗ A 1) . B 1; ∀ ( α ∗ A 2) . B 2� ρ ≜ ∀C 1 ∗ A 1 , C 2 ∗ A 2 , R ⊆ C 1 × C 2 .

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

20 X. Bi et al.

Now we have finally recovered the well-foundedness of the relation. It is again structurally inductive on the size of the type indexes.

Heterogeneous issues. We have not yet accounted for one major difference between the parametricity relation, from which we have borrowed ideas, and the canonicity relation, to which we have been adding. The former is homogeneous (i.e., the types of the two values is the same) and therefore has one type index, while the latter is heterogeneous (i.e., the two values may have different types) and therefore has two type indices. Thus we must also consider cases like V � α ; Int�. A definition that seems to handle this case appropriately is:

Here is an example to motivate it. Let E = Λ ( α∗⊤ ) . (( λx . x ) : α & Int → α & Int). We expect that E Int 1 evaluates to ⟨ 1 , 1 ⟩ . To prove that, we need to show (1 , 1) ∈ V � α ; Int�[ α�→ (Int , Int , R)]. According to Eq. (1), this is indeed the case. However, we run into ill-foundedness issue again, because ρ 1( α ) could be larger than α . Alas, this time the parametricity relation has no solution for us.

5.3 The Canonicity Relation for F[+] i

i

In light of the fact that substitution in the logical relation seems unavoidable in our setting, and that impredicativity is at odds with substitution, we turn to predicativity : we change rule T-tapp to its predicative version:

where metavariable t ranges over monotypes (types minus disjoint quantification). We do not believe that predicativity is a severe restriction in practice, since many source languages (e.g., those based on the Hindley-Milner type system [24, 32] like Haskell and OCaml) are themselves predicative and do not require the full generality of an impredicative core language.

Luckily, substitution with monotypes does not prevent well-foundedness. Figure 11 defines the canonicity relation for F[+] i[.][The][canonicity][relation][is][a][family] of binary relations over F co values that are heterogeneous , i.e., indexed by two F[+] i types. Two points are worth mentioning. (1) An apparent difference from λ[+] i[’s] logical relation is that our relation is now indexed by source types . The reason is that the type translation function (Definition 1) discards disjointness constraints, which are crucial in our setting, whereas λ[+] i[’s][type][translation][does][not][have][in-] formation loss. (2) Heterogeneity allows relating values of different types, and in particular values whose types are disjoint. The rationale behind the canonicity relation is to combine equality checking from traditional (homogeneous) logical relations with disjointness checking. It consists of two relations: the value relation V � A ; B � relates closed values; and the expression relation E � A ; B �—defined in terms of the value relation—relates closed expressions.

The relation V � A ; B � is defined by induction on the structures of A and B . For integers, it requires the two values to be literally the same. For two records to

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

Distributive Disjoint Polymorphism 21

( v 1 , v 2) ∈V �Int; Int� ≜ ∃i. v 1 = v 2 = i ( v 1 , v 2) ∈V � {l : A} ; {l : B } � ≜ ( v 1 , v 2) ∈V � A ; B � ( v 1 , v 2) ∈V � A 1 → B 1; A 2 → B 2� ≜ ∀ ( v 2 [′][,][ v][ ′] 1[)] [ ∈V][�] [A] 2[;] [ A] 1[�] [.][ (] [v] 1 [v][ ′] 1 [,][ v] 2 [v][ ′] 2[)] [ ∈E][�] [B] 1[;] [ B] 2[�] ( ⟨v 1 , v 2 ⟩, v 3) ∈V � A & B ; C � ≜ ( v 1 , v 3) ∈V � A ; C � ∧ ( v 2 , v 3) ∈V � B ; C �

( v 3 , ⟨v 1 , v 2 ⟩ ) ∈V � C ; A & B � ≜ ( v 3 , v 1) ∈V � C ; A � ∧ ( v 3 , v 2) ∈V � C ; B � ( v 1 , v 2) ∈V � ∀ ( α ∗ A 1) . B 1; ∀ ( α ∗ A 2) . B 2� ≜ ∀• ⊢ t ∗ A 1 & A 2 . ( v 1 |t|, v 2 |t| ) ∈E �[ t/α ] B 1; [ t/α ] B 2� ( v 1 , v 2) ∈V � A ; B � ≜ true otherwise ( e 1 , e 2) ∈E � A ; B � ≜ ∃v 1 , v 2 . e 1 −→[∗] v 1 ∧ e 2 −→[∗] v 2 ∧ ( v 1 , v 2) ∈V � A ; B �

behave the same, their fields must behave the same. For two functions to behave the same, they are required to produce outputs related at B 1 and B 2 when given related inputs at A 1 and A 2. For the next two cases regarding intersection types, the relation distributes over intersection constructor & . Of particular interest is the case for disjoint quantification. Notice that it does not quantify over arbitrary relations, but directly substitutes α with monotype t in B 1 and B 2. This means that our canonicity relation does not entail parametricity. However, it suffices for our purposes to prove coherence. Another noticeable thing is that we keep the invariant that A and B are closed types throughout the relation, so we no longer need to consider type variables. This simplifies things a lot. Note that when one type is ⊥ , two values are vacuously related because there simply are no values of type ⊥ . We need to show that the relation is indeed well-founded:

Lemma 5 (Well-foundedness). The canonicity relation of F[+] i[is well-founded.]

Proof. Let | · |∀ and | · |s be the number of ∀ -quantifies and the size of types, respectively. Consider the measure ⟨|·|∀, |·|s⟩ , where ⟨… ⟩ denotes lexicographic order. For the case of disjoint quantification, the number of ∀ -quantifiers decreases. For the other cases, the measure of | · |∀ does not increase, and the measure of | · |s strictly decreases. ⊓⊔

5.4 Establishing Coherence

Logical equivalence. The canonicity relation can be lifted to open expressions in the standard way, i.e., by considering all possible interpretations of free type and term variables. The logical interpretations of type and term contexts are found in the bottom half of Fig. 11.

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

22 X. Bi et al.

Definition 3 (Logical equivalence ⋍ log ).

∆ ; Γ ⊢ e 1 ⋍ log e 2 : A ; B ≜ |∆| ; |Γ | ⊢ e 1 : |A| ∧|∆| ; |Γ | ⊢ e 2 : |B | ∧

( ∀ρ, γ 1 , γ 2 . ρ ∈D � ∆ � ∧ ( γ 1 , γ 2) ∈G � Γ � ρ = ⇒ ( γ 1( ρ 1( e 1)) , γ 2( ρ 2( e 2))) ∈E � ρ ( A ); ρ ( B )�)

For conciseness, we write ∆ ; Γ ⊢ e 1 ⋍ log e 2 : A to mean ∆ ; Γ ⊢ e 1 ⋍ log e 2 : A ; A .

Contextual equivalence. Following λ[+] i[, the notion of coherence is based on] [ contex-] tual equivalence . The intuition is that two programs are equivalent if we cannot tell them apart in any context. As usual, contextual equivalence is expressed using expression contexts ( C and D denote F[+] i and F co expression contexts, respectively), Due to the bidirectional nature of the type system, the typing judgment of C features 4 different forms (full rules are in the appendix), e.g., C : ( ∆ ; Γ ⇒ A ) �→ ( ∆[′] ; Γ[′] ⇒ A[′] ) ⇝ D reads if ∆ ; Γ ⊢ E ⇒ A then ∆[′] ; Γ[′] ⊢C{E } ⇒ A[′] . The judgment also generates a well-typed F co context D . The following two definitions capture the notion of contextual equivalence:

Definition 4 (Kleene Equality ⋍ ). Two complete programs (i.e., closed terms of type Int ), e and e[′] , are Kleene equal, written e ⋍ e[′] , iff there exists an integer i such that e −→[∗] i and e[′] −→[∗] i.

Definition 5 (Contextual Equivalence ⋍ ctx ).

∆ ; Γ ⊢ E 1 ⋍ ctx E 2 : A ≜ ∀e 1 , e 2 . ∆ ; Γ ⊢ E 1 ⇒ A ⇝ e 1 ∧ ∆ ; Γ ⊢ E 2 ⇒ A ⇝ e 2 ∧ ( ∀C , D. C : ( ∆ ; Γ ⇒ A ) �→ ( • ; • ⇒ Int) ⇝ D = ⇒D{e 1 } ⋍ D{e 2 } )

Coherence. For space reasons, we directly show the coherence statement of F[+] i[.] We need several technical lemmas such as compatibility lemmas, fundamental property, etc. The interested reader can refer to our Coq formalization.

Theorem 5 (Coherence). We have that

That is, coherence is a special case of Definition 5 where E 1 and E 2 are the same. At first glance, this appears underwhelming: of course E behaves the same as itself! The tricky part is that, if we expand it according to Definition 5, it is not E itself but all its translations e 1 and e 2 that behave the same!

6 Related Work

Coherence. In calculi featuring coercive subtyping, a semantics that interprets the subtyping judgment by introducing explicit coercions is typically defined on typing derivations rather than on typing judgments. A natural question that arises for such systems is whether the semantics is coherent , i.e., distinct typing derivations of the same typing judgment possess the same meaning. Since Reynolds [45] proved the coherence of a calculus with intersection types, many

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

Distributive Disjoint Polymorphism 23

researchers have studied the problem of coherence in a variety of typed calculi. Two approaches are commonly found in the literature. 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 judgment [8, 15, 47]. However, this approach cannot be directly applied to Curry-style calculi (where the lambda abstractions are not type annotated). Biernacki and Polesiuk [6] considered the coherence problem of coercion semantics. Their criterion for coherence of the translation is contextual equivalence in the target calculus. Inspired by this approach, Bi et al. [5] proposed the canonicity relation to prove coherence for a calculus with disjoint intersection types and BCD subtyping. As we have shown in Section 5, constructing a suitable logical relation for F[+] i[is][challenging.][On][the][one][hand,] the original approach by Alpuim et al. [2] in F i does not work any more due to the addition of BCD subtyping. On the other hand, simply combining System F’s logical relation with λ[+] i[’s canonicity relation does not work as expected, due] to the issue of well-foundedness. To solve the problem, we employ immediate substitutions and a restriction to predicative instantiations.

BCD subtyping and decidability. The BCD type system was first introduced by Barendregt et al. [3] 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. The decidability of BCD subtyping has been shown in several works [27, 38, 41, 51]. Laurent [28] formalized the relation in Coq in order to eliminate transitivity cuts from it, but his formalization does not deliver an algorithm. Only recently, Laurent [30] presented a general way of defining a BCD-like subtyping relation extended with generic contravariant/covariant type constructors that enjoys the “sub-formula property”. Our Coq formalization extends the approach used in λ[+] i[,][which][follows][a][different][idea] based on Pierce’s decision procedure [38], with parametric (disjoint) polymorphism and corresponding distributivity rules. More recently, Muehlboeck and Tate [34] presented a decidable algorithmic system (proved in Coq) with union and intersection types. Similar to F[+] i[, their system also has distributive subtyping] rules. They also discussed the addition of polymorphism, but left a Coq formalization for future work. In their work they regard intersections of disjoint types (e.g., String & Int) as uninhabitable, which is different from our interpretation. As a consequence, coherence is a non-issue for them.

Intersection types, the merge operator and polymorphism. Forsythe [44] has intersection types and a merge-like operator. However to ensure coherence, various restrictions were added to limit the use of merges. In Forsythe merges cannot contain more than one function. Castagna et al. [12] proposed a coherent calculus λ & to study overloaded functions. λ & has a special merge operator that works on functions only. Dunfield proposed a calculus [16] (which we call λ,, ) that shows significant expressiveness of type systems with unrestricted intersection types and an (unrestricted) merge operator. However, because of his unrestricted merge operator (allowing 1 , , 2), his calculus lacks coherence. Blaauwbroek’s λ[∨] ∧7[enriched] [λ][,,][with][BCD][subtyping][and][computational][effects,][but]

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

24 X. Bi et al.

	λ,, [16]	λi [36]	λ∨ ∧[7]	λ+ i [5]	F_i_ [2]	F+ i
Disjointness
Unrestricted intersections
BCD subtyping
Polymorphism
Coherence
Bottom type

Fig. 12: Summary of intersection calculi ( = yes, = no, = syntactic coherence)

he did not address coherence. The coherence issue for a calculus similar to λ,, was first addressed in λi [36] with the notion of disjointness, but at the cost of dropping unrestricted intersections, and a strict notion of coherence (based on α -equivalence). Later Bi et al. [5] improved calculi with disjoint intersection types by removing several restrictions, adopted BCD subtyping and a semantic notion of coherence (based on contextual equivalence) proved using canonicity. The combination of intersection types, a merge operator and parametric polymorphism, while achieving coherence was first studied in F i [2], which serves as a foundation for F[+] i[. However,][ F] [i][suffered the same problems as] [ λ][i][. Additionally] in F i a bottom type is problematic due to interactions with disjoint polymorphism and the lack of unrestricted intersections. The issues can be illustrated with the well-typed F[+] i[expression] [Λ][(] [α][ ∗⊥][)] [. λ][x][:] [ α.][ x][ , ,][x][.][In][this][expression][the] type of x , , x is α & α . Such a merge does not violate disjointness because the only types that α can be instantiated with are top-like, and top-like types do not introduce incoherence. In F i a type variable α can never be disjoint to another type that contains α , but (as the previous expression shows) the addition of a bottom type allows expressions where such (strict) condition does not hold. In this work, we removed those restrictions, extended BCD subtyping with polymorphism, and proposed a more powerful logical relation for proving coherence. Figure 12 summarizes the main differences between the aforementioned calculi.

There are also several other calculi with intersections and polymorphism. Pierce proposed F ∧ [39], a calculus combining intersection types and bounded quantification. Pierce translates F ∧ to System F extended with products, but he left coherence as a conjecture. More recently, Castagna et al. [14] proposed a polymorphic calculus with set-theoretic type connectives (intersections, unions, negations). But their calculus does not include a merge operator. Castagna and Lanvin also proposed a gradual type system [13] with intersection and union types, but also without a merge operator.

Row polymorphism and bounded polymorphism. Row polymorphism was originally proposed by Wand [54] as a mechanism to enable type inference for a simple object-oriented language based on recursive records. These ideas were later adopted into type systems for extensible records [19, 21, 31]. Our merge operator can be seen as a generalization of record extension/concatenation, and selection is also built-in. In contrast to most record calculi, restriction is not a primitive

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

Distributive Disjoint Polymorphism 25

operation in F[+] i[, but can be simulated via subtyping. Disjoint quantification can] simulate the lacks predicate often present in systems with row polymorphism. Recently Morris and McKinna presented a typed language [33], generalizing and abstracting existing systems of row types and row polymorphism. Alpuim et al. [2] informally studied the relationship between row polymorphism and disjoint polymorphism, but it would be interesting to study such relationship more formally. The work of Morris and McKinna may be interesting for such study in that it gives a general framework for row type systems.

Bounded quantification is currently the dominant mechanism in major mainstream object-oriented languages supporting both subtyping and polymorphism. F < : [10] provides a simple model for bounded quantification, but type-checking in full F < : is proved to be undecidable [40]. Pierce’s thesis [39] discussed the relationship between calculi with simple polymorphism and intersection types and bounded quantification. He observed that there is a way to “encode” many forms of bounded quantification in a system with intersections and pure (unbounded) second-order polymorphism. That encoding can be easily adapted to F[+] i[:]

∀ ( α < : A ) . B ≜ ∀ ( α ∗⊤ ) . ([ A & α/α ] B )

The idea is to replace bounded quantification by (unrestricted) universal quantification and all occurrences of α by A & α in the body. Such an encoding seems to indicate that F[+] i could be used as a decidable alternative to (full) F < :. It is worthwhile to note that this encoding does not work in F i because A & α is not well-formed ( α is not disjoint to A ). In other words, the encoding requires unrestricted intersections.

7 Conclusion and Future Work

We have proposed F[+] i[, a type-safe and coherent calculus with disjoint intersection] types, BCD subtyping and parametric polymorphism. F[+] i[improves][the][state-of-] art of compositional designs, and enables the development of highly modular and reusable programs. One interesting and useful further extension would be implicit polymorphism. For that we want to combine Dunfield and Krishnaswami’s approach [17] with our bidirectional type system. We would also like to study the parametricity of F[+] i[.][As][we][have][seen][in][Section][5.2,][it][is][not][at][all][obvious][how] to extend the standard logical relation of System F to account for disjointness, and avoid potential circularity due to impredicativity. A promising solution is to use step-indexed logical relations [1].

Acknowledgments

We thank the anonymous reviewers and Yaoda Zhou for their helpful comments. This work has been sponsored by the Hong Kong Research Grant Council projects number 17210617 and 17258816, and by the Research Foundation - Flanders.

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

Bibliography

• [1] Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: European Symposium on Programming (ESOP) (2006)

• [2] Alpuim, J., Oliveira, B.C.d.S., Shi, Z.: Disjoint polymorphism. In: European Symposium on Programming (ESOP) (2017)

• [3] Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. The journal of symbolic logic 48 (04), 931–940 (1983)

• [4] Bi, X., Oliveira, B.C.d.S.: Typed First-Class Traits. In: European Conference on Object-Oriented Programming (ECOOP) (2018)

• [5] Bi, X., Oliveira, B.C.d.S., Schrijvers, T.: The Essence of Nested Composition. In: European Conference on Object-Oriented Programming (ECOOP) (2018)

• [6] Biernacki, D., Polesiuk, P.: Logical relations for coherence of effect subtyping. In: International Conference on Typed Lambda Calculi and Applications (TLCA) (2015)

• [7] Blaauwbroek, L.: On the Interaction Between Unrestricted Union and Intersection Types and Computational Effects. Master’s thesis, Technical University Eindhoven (2017)

• [8] Breazu-Tannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as implicit coercion. Information and Computation 93 (1), 172–221 (1991)

• [9] Brent, R.P., Kung, H.T.: The chip complexity of binary arithmetic. In: Proceedings of the twelfth annual ACM symposium on Theory of computing. pp. 190–200 (1980)

• [10] Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys 17 (4), 471–523 (1985)

• [11] Carette, J., Kiselyov, O., Shan, C.C.: Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19 (05), 509 (2009)

• [12] Castagna, G., Ghelli, G., Longo, G.: A calculus for overloaded functions with subtyping. In: Conference on LISP and Functional Programming (1992)

• [13] Castagna, G., Lanvin, V.: Gradual typing with union and intersection types. Proceedings of the ACM on Programming Languages 1 (ICFP), 1–28 (aug 2017)

• [14] Castagna, G., Nguyen, K., Xu, Z., Im, H., Lenglet, S., Padovani, L.: Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In: Principles of Programming Languages (POPL) (2014)

• [15] Curien, P.L., Ghelli, G.: Coherence of subsumption, minimum typing and type-checking in f ≤ . Mathematical Structures in Computer Science (MSCS) 2 (01), 55 (1992)

• [16] Dunfield, J.: Elaborating intersection and union types. Journal of Functional Programming (JFP) 24 (2-3), 133–165 (2014)

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

Distributive Disjoint Polymorphism 27

• [17] Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. In: International Conference on Functional Programming (ICFP) (2013)

• [18] Fokkinga, M.M.: Tupling and mutumorphisms. Squiggolist 1 (4) (1989)

• [19] Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records and variants. Tech. rep., University of Nottingham (1996)

• [20] Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow embeddings (functional pearl). In: ICFP. pp. 339–347. ACM (2014)

• [21] Harper, R., Pierce, B.: A record calculus based on symmetric concatenation. In: Principles of Programming Languages (POPL) (1991)

• [22] Henglein, F.: Dynamic typing: syntax and proof theory. Science of Computer Programming 22 (3), 197–230 (6 1994)

• [23] Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. HigherOrder and Symbolic Computation 23 (2), 167 (2010)

• [24] Hindley, R.: The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society 146 , 29–60 (1969)

• [25] Hinze, R.: An algebra of scans. In: International Conference on Mathematics of Program Construction. pp. 186–210 (2004)

• [26] Hofer, C., Ostermann, K., Rendel, T., Moors, A.: Polymorphic embedding of DSLs. In: International Conference on Generative Programming and Component Engineering (GPCE) (2008)

• [27] Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. Typed Lambda Calculi and Applications pp. 297–311 (1995)

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

• [29] Laurent, O.: A syntactic introduction to intersection types (2012), unpublished note

• [30] Laurent, O.: Intersection subtyping with constructors. In: Proceedings of the Ninth Workshop on Intersection Types and Related Systems (2018)

• [31] Leijen, D.: Extensible records with scoped labels. Trends in Functional Programming 5 , 297–312 (2005)

• [32] Milner, R.: A theory of type polymorphism in programming. Journal of computer and system sciences 17 (3), 348–375 (1978)

• [33] Morris, J.G., McKinna, J.: Abstracting extensible data types. In: Principles of Programming Languages (POPL) (2019)

• [34] Muehlboeck, F., Tate, R.: Empowering union and intersection types with integrated subtyping. In: OOPSLA (2018)

• [35] Oliveira, B.C.d.S., Cook, W.R.: Extensibility for the masses. In: European Conference on Object-Oriented Programming (ECOOP) (2012)

• [36] Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: International Conference on Functional Programming (ICFP) (2016)

• [37] Oliveira, B.C.d.S., Van Der Storm, T., Loh, A., Cook, W.R.: Featureoriented programming with object algebras. In: European Conference on Object-Oriented Programming (ECOOP) (2013)

• [38] Pierce, B.C.: A decision procedure for the subtype relation on intersection types with bounded variables. Tech. rep., Carnegie Mellon University (1989)

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

28 X. Bi et al.

• [39] Pierce, B.C.: Programming with intersection types and bounded polymorphism. Ph.D. thesis, University of Pennsylvania (1991)

• [40] Pierce, B.C.: Bounded quantification is undecidable. Information and Computation 112 (1), 131–165 (1994)

• [41] Rehof, J., Urzyczyn, P.: Finite combinatory logic with intersection types. In: International Conference on Typed Lambda Calculi and Applications (2011)

• [42] Rendel, T., Brachth¨auser, J.I., Ostermann, K.: From object algebras to attribute grammars. In: Object-Oriented Programming, Systems Languages and Applications (OOPSLA) (2014)

• [43] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Proceedings of the IFIP 9th World Computer Congress (1983)

• [44] Reynolds, J.C.: Preliminary design of the programming language forsythe. Tech. rep., Carnegie Mellon University (1988)

• [45] Reynolds, J.C.: The coherence of languages with intersection types. In: Lecture Notes in Computer Science (LNCS), pp. 675–700. Springer Berlin Heidelberg (1991)

• [46] d. S. Oliveira, B.C., Hinze, R., L¨oh, A.: Extensible and modular generics for the masses. In: Revised Selected Papers from the Seventh Symposium on Trends in Functional Programming, TFP 2006, Nottingham, United Kingdom, 19-21 April 2006. pp. 199–216 (2006)

• [47] Schwinghammer, J.: Coherence of subsumption for monadic types. Journal of Functional Programming (JFP) 19 (02), 157 (2008)

• [48] Scott, D.: Outline of a mathematical theory of computation. Oxford University Computing Laboratory, Programming Research Group (1970)

• [49] Scott, D.S., Strachey, C.: Toward a mathematical semantics for computer languages, vol. 1. Oxford University Computing Laboratory, Programming Research Group (1971)

• [50] Siek, J., Thiemann, P., Wadler, P.: Blame and coercion: together again for the first time. In: Conference on Programming Language Design and Implementation (PLDI) (2015)

• [51] Statman, R.: A finite model property for intersection types. Electronic Proceedings in Theoretical Computer Science 177 , 1–9 (2015)

• [52] Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’89 (1989)

• [53] Wadler, P.: The expression problem. Java-genericity mailing list (1998)

• [54] Wand, M.: Complete type inference for simple objects. In: Symposium on Logic in Computer Science (LICS) (1987)

• [55] Zhang, W., d. S. Oliveira, B.C.: Shallow edls and object-oriented programming. To appear in Programming Journal (2019)

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