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 coherence) 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.
