Distributive Disjoint Polymorphism for Compositional Programming
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.
Tue 9 Apr Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30: TypesESOP at SUN II Chair(s): Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon | |||
10:30 - 11:00 Talk | Handling polymorphic algebraic effects ESOP Link to publication | ||
11:00 - 11:30 Talk | Distributive Disjoint Polymorphism for Compositional Programming ESOP Xuan BiStandard Chartered Bank, Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven Link to publication | ||
11:30 - 12:00 Talk | Types by Need ESOP Link to publication | ||
12:00 - 12:30 Talk | Verifiable certificates for predicate subtyping ESOP Link to publication |