Direct Foundations for Compositional Programming

Authors Andong Fan , Xuejing Huang , Han Xu , Yaozhu Sun, Bruno C. d. S. Oliveira

Thumbnail PDF


  • Filesize: 1.13 MB
  • 28 pages

Document Identifiers

Author Details

Andong Fan
  • Zhejiang University, Hangzhou, China
Xuejing Huang
  • The University of Hong Kong, China
Han Xu
  • Peking University, Beijing, China
Yaozhu Sun
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China


We thank the anonymous reviewers and Wenjia Ye for their helpful comments.

Cite AsGet BibTex

Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. Direct Foundations for Compositional Programming. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 18:1-18:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


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

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Intersection types
  • disjoint polymorphism
  • operational semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In European Symposium on Programming (ESOP), 2006. Google Scholar
  2. João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European Symposium on Programming (ESOP), 2017. Google Scholar
  3. Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, September 2001. Google Scholar
  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. Google Scholar
  5. Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits. In European Conference on Object-Oriented Programming (ECOOP), 2018. Google Scholar
  6. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition. In European Conference on Object-Oriented Programming (ECOOP), 2018. Google Scholar
  7. Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint polymorphism for compositional programming. In European Symposium on Programming (ESOP), 2019. Google Scholar
  8. Kim B Bruce, Luca Cardelli, and Benjamin C Pierce. Comparing object encodings. In International Symposium on Theoretical Aspects of Computer Software, pages 415-438. Springer, 1997. Google Scholar
  9. Luca Cardelli and John C Mitchell. Operations on records. In International Conference on Mathematical Foundations of Programming Semantics, 1989. Google Scholar
  10. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-523, 1985. Google Scholar
  11. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In Conference on LISP and Functional Programming, 1992. Google Scholar
  12. William R. Cook. A Denotational Semantics of Inheritance. PhD thesis, Brown University, 1989. Google Scholar
  13. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming (ICFP), 2000. Google Scholar
  14. Jana Dunfield. Elaborating intersection and union types. Journal of Functional Programming (JFP), 24(2-3):133-165, 2014. Google Scholar
  15. Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Comput. Surv., 54(5), May 2021. URL:
  16. Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming (ECOOP), 2001. Google Scholar
  17. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  18. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Type classes in haskell. ACM Trans. Program. Lang. Syst., 18(2):109-138, March 1996. Google Scholar
  19. Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Principles of Programming Languages (POPL), 1991. Google Scholar
  20. Xuejing Huang and Bruno C. d. S. Oliveira. A type-directed operational semantics for a calculus with a merge operator. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:32, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL:
  21. Xuejing Huang and Bruno C d S Oliveira. Distributing intersection and union types with splits and duality (functional pearl). Proceedings of the ACM on Programming Languages, 5(ICFP):1-24, 2021. Google Scholar
  22. Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. Taming the merge operator. Journal of Functional Programming, 31:e28, 2021. URL:
  23. Stefan Kaes. Parametric overloading in polymorphic programming languages. In H. Ganzinger, editor, ESOP '88, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg. Google Scholar
  24. Daan Leijen. Extensible records with scoped labels. Trends in Functional Programming, 5:297-312, 2005. Google Scholar
  25. Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, pages 333-343, 1995. Google Scholar
  26. Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated subtyping. In OOPSLA, 2018. Google Scholar
  27. Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. Simplicitly: Foundations and applications of implicit function types. Proc. ACM Program. Lang., 2(POPL), December 2017. Google Scholar
  28. Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA '95, pages 135-146, New York, NY, USA, 1995. Association for Computing Machinery. Google Scholar
  29. Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects and implicits. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA, pages 341-360. ACM, 2010. URL:
  30. Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In International Conference on Functional Programming (ICFP), 2016. Google Scholar
  31. Benjamin C Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical report, Carnegie Mellon University, 1989. Google Scholar
  32. Benjamin C Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131-165, 1994. Google Scholar
  33. John C Reynolds. Towards a theory of type structure. In Programming Symposium, pages 408-425. Springer, 1974. Google Scholar
  34. John C Reynolds. Preliminary design of the programming language forsythe. Technical report, Carnegie Mellon University, 1988. Google Scholar
  35. John C. Reynolds. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS), pages 675-700. Springer Berlin Heidelberg, 1991. Google Scholar
  36. John C Reynolds. Design of the programming language forsythe. In ALGOL-like languages, pages 173-233. Birkhauser Boston Inc., 1997. Google Scholar
  37. Tom Schrijvers and Bruno C. d. S. Oliveira. Monads, zippers and views: virtualizing the monad stack. In Proceedings of the 16th ACM SIGPLAN international conference on functional programming, pages 32-44, 2011. Google Scholar
  38. Mark Shields and Erik Meijer. Type-indexed rows. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 261-275, New York, NY, USA, 2001. Association for Computing Machinery. URL:
  39. Jeremy G. Siek. Transitivity of subtyping for intersection types. CoRR, abs / 1906.09709, 2019. URL:
  40. Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006. Google Scholar
  41. Jeremy G. Siek and Walid Taha. Gradual typing for objects. In Erik Ernst, editor, ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings, volume 4609 of Lecture Notes in Computer Science, pages 2-27. Springer, 2007. Google Scholar
  42. Philip Wadler. The expression problem. Java-genericity mailing list, 1998. Google Scholar
  43. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 60-76. ACM Press, 1989. URL:
  44. Ningning Xie, Bruno C d S Oliveira, Xuan Bi, and Tom Schrijvers. Row and bounded polymorphism via disjoint polymorphism. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. Google Scholar
  45. Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-directed operational semantics for gradual typing. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 12:1-12:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  46. Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. Compositional programming. ACM Transactions on Programming Languages and Systems (TOPLAS), 43(3):1-61, 2021. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail