Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-22T13:31:07.595Z Has data issue: false hasContentIssue false
  • English
  • Français

Taming the Merge Operator

Published online by Cambridge University Press:  02 November 2021

XUEJING HUANG Open the ORCID record for XUEJING HUANG [Opens in a new window] ,
JINXU ZHAO  and
BRUNO C. D. S. OLIVEIRA
XUEJING HUANG
Affiliation:
Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong (e-mail: [email protected])
JINXU ZHAO
Affiliation:
Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong (e-mail: [email protected])
BRUNO C. D. S. OLIVEIRA
Affiliation:
Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition, and simple solutions to hard modularity problems. Unfortunately, recent calculi with disjoint intersection types and the merge operator lack a (direct) operational semantics with expected properties such as determinism and subject reduction, and only account for terminating programs. This paper proposes a type-directed operational semantics (TDOS) for calculi with intersection types and a merge operator. We study two variants of calculi in the literature. The first calculus, called λi, is a variant of a calculus presented by Oliveira et al. (2016) and closely related to another calculus by Dunfield (2014). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject reduction. Using our TDOS, we obtain a direct semantics for λi that has both properties. The second calculus, called λi+, employs the well-known subtyping relation of Barendregt, Coppo and Dezani-Ciancaglini (BCD). Therefore, λi+ extends the more basic subtyping relation of λi, and also adds support for record types and nested composition (which enables recursive composition of merged components). To fully obtain determinism, both λi and λi+ employ a disjointness restriction proposed in the original λi calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike previous calculi with disjoint intersection types where recursion is problematic. We relate the static and dynamic semantics of λi to the original version of the calculus and the calculus by Dunfield. Furthermore, for λi+, we show a novel formulation of BCD subtyping, which is algorithmic, has a very simple proof of transitivity and allows for the modular addition of distributivity rules (i.e. without affecting other rules of subtyping). All results have been fully formalized in the Coq theorem prover.

Type
Research Article
Information
Journal of Functional Programming , Volume 31 , 2021 , e28
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Ahmed, A. J. (2006) Step-indexed syntactic logical relations for recursive and quantified types. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Proceedings. Springer, pp. 69–83.CrossRefGoogle Scholar
Alpuim, J., d. S. Oliveira, B. C. & Shi, Z. (2017) Disjoint polymorphism. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Springer, pp. 1–28.CrossRefGoogle Scholar
Barbanera, F., Dezani-Ciancaglini, M. & De’Liguoro, U. (1995) Intersection and union types: Syntax and semantics. Inform. Comput. 119(2), 202–230.CrossRefGoogle Scholar
Barendregt, H. (1984) The Lambda Calculus - Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics.Google Scholar
Barendregt, H., Coppo, M. & Dezani-Ciancaglini, M. (1983) A filter lambda model and the completeness of type assignment. J. Symb. Logic 48(4).CrossRefGoogle Scholar
Bessai, J., Dudenhefner, A., Düdder, B. & Rehof, J. (2016) Extracting a formally verified subtyping algorithm for intersection types from ideals and filters. TYPES.Google Scholar
Bessai, J., Rehof, J. & Düdder, B. (2019) Fast verified BCD subtyping. In Models, Mindsets, Meta: The What, the How, and the Why Not?, vol. 11200. Lecture Notes in Computer Science. Cham: Springer, pp. 356–371.CrossRefGoogle Scholar
Bi, X., d. S. Oliveira, B. C. & Schrijvers, T. (2018) The essence of nested composition. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16–21, 2018, Amsterdam, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 22:1–22:33.Google Scholar
Bi, X. & Oliveira, B. C. d. S. (2018) Typed first-class traits. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 9:1–9:28.Google Scholar
Bi, X., Xie, N., d. S. Oliveira, B. C. & Schrijvers, T. (2019) Distributive disjoint polymorphism for compositional programming. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Springer, pp. 381–409.CrossRefGoogle Scholar
Bracha, G. & Cook, W. R. (1990) Mixin-based inheritance. In Conference on Object-Oriented Programming Systems, Languages, and Applications/European Conference on Object-Oriented Programming (OOPSLA/ECOOP), Ottawa, Canada, October 21-25, 1990, Proceedings. ACM, pp. 303–311.CrossRefGoogle Scholar
Büchi, M. & Weck, W. (2000) Generic wrappers. In European Conference on Object-Oriented Programming (ECOOP).CrossRefGoogle Scholar
Cardelli, L. (1992) Extensible Records in a Pure Calculus of Subtyping. Digital. Systems Research Center.Google Scholar
Cardelli, L. & Mitchell, J. (1991) Operations on records. Math. Struct. Comput. Sci. 1, 3–48.CrossRefGoogle Scholar
Cardelli, L. & Wegner, P. (1985) On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–522.CrossRefGoogle Scholar
Castagna, G., Ghelli, G. & Longo, G. (1995) A calculus for overloaded functions with subtyping. Inf. Comput. 117(1), 115–135.CrossRefGoogle Scholar
Castagna, G., Nguyen, K., Xu, Z. & Abate, P. (2015) Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. ACM, pp. 289–302.CrossRefGoogle Scholar
Castagna, G., Nguyen, K., Xu, Z., Im, H., Lenglet, S. & Padovani, L. (2014) Polymorphic functions with set-theoretic types: part 1: Syntax, semantics, and evaluation. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, 2014. ACM, pp. 5–18.CrossRefGoogle Scholar
Castagna, G. & Xu, Z. (2011) Set-theoretic foundation of parametric polymorphism and subtyping. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011. ACM. pp. 94–106.CrossRefGoogle Scholar
Chakravarty, M. M. T., Keller, G. & Jones, S. L. P. (2005a) Associated type synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26–28, 2005. ACM, pp. 241–253.Google Scholar
Chakravarty, M. M. T., Keller, G., Jones, S. L. P. & Marlow, S. (2005b) Associated types with class. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. ACM, pp. 1–13.CrossRefGoogle Scholar
Chambers, C. & Chen, W. (1999) Efficient multiple and predicated dispatching. In Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 1999), Denver, Colorado, USA, November 1-5, 1999. ACM, pp. 238–255.CrossRefGoogle Scholar
Chlipala, A. (2010) Ur: statically-typed metaprogramming with type-level record computation. ACM Sigplan Not. 45(6), 122–133.CrossRefGoogle Scholar
Clifton, C., Leavens, G. T., Chambers, C. & Millstein, T. D. (2000) Multijava: Modular open classes and symmetric multiple dispatch for java. In Proceedings of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 2000), Minneapolis, Minnesota, USA, October 15–19, 2000. ACM, pp. 130–145.CrossRefGoogle Scholar
Compagnoni, A. B. & Goguen, H. (2003) Typed operational semantics for higher-order subtyping. Inf. Comput. 184(2), 242–297.CrossRefGoogle Scholar
Cook, W. R. & Palsberg, J. (1989) A denotational semantics of inheritance and its correctness. In Object-Oriented Programming: Systems, Languages and Applications (OOPSLA).CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M. & Venneri, B. (1981) Functional characters of solvable terms. Math. Log. Q. 27(2-6), 45–58.CrossRefGoogle Scholar
Davies, R. & Pfenning, F. (2000) Intersection types and computational effects. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 18–21, 2000. ACM. pp. 198–208.CrossRefGoogle Scholar
Devriese, D. & Piessens, F. (2011) On the bright side of type classes: Instance arguments in Agda. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011. ACM. pp. 143–155.CrossRefGoogle Scholar
Dunfield, J. (2014) Elaborating intersection and union types. J. Funct. Program. 24(2–3), 133–165.CrossRefGoogle Scholar
Dunfield, J. & Pfenning, F. (2003) Type assignment for intersections and unions in call-by-value languages. In Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003, Warsaw, Poland, Proceedings. Springer, 250–266.CrossRefGoogle Scholar
Ernst, E. (2001) Family polymorphism. In Proceedings of the 15th European Conference on Object-Oriented Programming. Berlin, Heidelberg: Springer-Verlag, p. 303–326.CrossRefGoogle Scholar
Facebook. (2014) Flow. https://flow.org/ Google Scholar
Feng, Y. & Luo, Z. (2009) Typed operational semantics for dependent record types. In Proceedings Types for Proofs and Programs, Revised Selected Papers, TYPES 2009, Aussois, France, 12-15th May 2009. pp. 30–46.Google Scholar
Fisher, K. & Mitchell, J. (1995) A delegation-based object calculus with subtyping. Fundamentals of Computation Theory. CrossRefGoogle Scholar
Flatt, M., Krishnamurthi, S. & Felleisen, M. (1998) Classes and mixins. In POPL 1998, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998. ACM, pp. 171–183.CrossRefGoogle Scholar
Freeman, T. S. & Pfenning, F. (1991) Refinement types for ML. In Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI). ACM, pp. 268–277.CrossRefGoogle Scholar
Goguen, H. (1994) A Typed Operational Semantics for Type Theory. Ph.D. thesis. University of Edinburgh, UK.CrossRefGoogle Scholar
Goguen, H. (1995) Typed operational semantics. In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA 1995, 1995, Proceedings. Springer, pp. 186–200.CrossRefGoogle Scholar
Hall, C. V., Hammond, K., Jones, S. L. P. & Wadler, P. (1996) Type classes in haskell. ACM Trans. Program. Lang. Syst. 18(2), 109–138.Google Scholar
Harper, R. & Pierce, B. (1991) A record calculus based on symmetric concatenation. In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: Association for Computing Machinery, pp. 131–142.CrossRefGoogle Scholar
Huang, X. & Oliveira, B. C. d. S. (2020) A type-directed operational semantics for a calculus with a merge operator. In 34th European Conference on Object-Oriented Programming, ECOOP 2020.Google Scholar
Kaes, S. (1988) Parametric overloading in polymorphic programming languages. In ESOP 1988, 2nd European Symposium on Programming, Proceedings. Springer, pp. 131–144.CrossRefGoogle Scholar
Kniesel, G. (1999) Type-safe delegation for runtime component adaptation. In European Conference on Object-Oriented Programming (ECOOP).CrossRefGoogle Scholar
Knuth, D. E. (1971) Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages. Springer.CrossRefGoogle Scholar
Kurata, T. & Takahashi, M. (1995) Decidable properties of intersection type systems. In Proceedings of the Second International Conference on Typed Lambda Calculi and Applications. Springer-Verlag, p. 297–311.CrossRefGoogle Scholar
Laurent, O. (2012) Intersection types with subtyping by means of cut elimination. Fundamenta Informaticae. 121(1–4), 203–226.CrossRefGoogle Scholar
Laurent, O. (2019) Intersection subtyping with constructors. In Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems (DCM 2018 and ITRS 2018), pp. 73–84.CrossRefGoogle Scholar
Leijen, D. (2004) First-class labels for extensible rows. Technical Report UU-CS-2004-51. Dept. of Computer Science, Universiteit Utrecht. UTCS Technical Report.Google Scholar
Lieberman, H. (1986) Using prototypical objects to implement shared behavior in object oriented systems. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA).CrossRefGoogle Scholar
Luo, Z. (1999) Coercive subtyping. J. Log. Comput. 9(1), 105–130.CrossRefGoogle Scholar
Microsoft. (2012) TypeScript. https://www.typescriptlang.org/ Google Scholar
Muehlboeck, F. & Tate, R. (2018) Empowering union and intersection types with integrated subtyping. Proc. ACM Program. Lang. 2(OOPSLA), 112:1–112:29.CrossRefGoogle Scholar
Muschevici, R., Potanin, A., Tempero, E. D. & Noble, J. (2008) Multiple dispatch in practice. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN, USA. ACM, pp. 563–582.CrossRefGoogle Scholar
Nierstrasz, O., Ducasse, S. & Schärli, N. (2006) Flattening traits. Journal of Object Technology. 5(4), 129–148.CrossRefGoogle Scholar
Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E. & Zenger, M. (2004) An overview of the Scala programming language. Technical report. École Polytechnique Fédérale de Lausanne.Google Scholar
Odersky, M., Wadler, P. & Wehr, M. (1995) A second look at overloading. In Proceedings of the Seventh International Conference on Functional Programming languages and Computer Architecture, FPCA 1995. ACM, pp. 135–146.CrossRefGoogle Scholar
Oliveira, B. C. d. S., Moors, A. & Odersky, M. (2010) Type classes as objects and implicits. In 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. ACM, pp. 341–360.CrossRefGoogle Scholar
Oliveira, B. C. d. S., Shi, Z. & Alpuim, J. (2016) Disjoint intersection types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016. ACM, pp. 364–377.CrossRefGoogle Scholar
Ostermann, K. (2002) Dynamically composable collaborations with delegation layers. In European Conference on Object-Oriented Programming (ECOOP).CrossRefGoogle Scholar
Palsberg, J. & Zhao, T. (2004) Type inference for record concatenation and subtyping. Inf. Comput. 189(1), 54–86.CrossRefGoogle Scholar
Park, G., Hong, J. Jr, G. L. S. & Ryu, S. (2019) Polymorphic symmetric multiple dispatch with variance. Proc. ACM Program. Lang. 3(POPL), 11:1–11:28.CrossRefGoogle Scholar
Pierce, B. & Steffen, M. (1997) Higher-order subtyping. Theor. Comput. Sci. 176(1), 235–282.CrossRefGoogle Scholar
Pierce, B. C. (1989) A decision procedure for the subtype relation on intersection types with bounded variables. Technical report. School of Computer Science, Carnegie-Mellon University.Google Scholar
Pierce, B. C. (1991) Programming with Intersection Types and Bounded Polymorphism. Ph.D. thesis. Carnegie Mellon University.Google Scholar
Pierce, B. C. & Turner, D. N. (1998) Local type inference. In Proceedings of ACM Symposium on Principles of Programming Languages, pp. 252–265.CrossRefGoogle Scholar
Plotkin, G. (1973) Lambda-definability and logical relations.Google Scholar
Poll, E. (1997) System F with width-subtyping and record updating. In International Symposium on Theoretical Aspects of Computer Software. Springer, pp. 439–457.CrossRefGoogle Scholar
Pottier, F. (2000) A 3-part type inference engine. In European Symposium on Programming. Springer, pp. 320–335.CrossRefGoogle Scholar
Pottinger, G. (1980) A type assignment for the strongly normalizable λ-terms. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577.Google Scholar
RedHat. (2011) Ceylon. https://ceylon-lang.org/ Google Scholar
Rehof, J. & Urzyczyn, P. (2011) Finite combinatory logic with intersection types. In International Conference on Typed Lambda Calculi and Applications.CrossRefGoogle Scholar
Rémy, D. (1989) Type checking records and variants in a natural extension of ML. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 77–88.CrossRefGoogle Scholar
Rémy, D. (1995) A case study of typechecking with constrained types: Typing record concatenation. In Presented at the workshop on Advances in Types for Computer Science at the Newton Institute, Cambridge, UK.Google Scholar
Reynolds, J. C. (1988) Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159. Carnegie Mellon University.Google Scholar
Reynolds, J. C. (1991) The coherence of languages with intersection types. In Theoretical Aspects of Computer Software, International Conference TACS 1991, Sendai, Japan, September 24-27, 1991, Proceedings. Springer, pp. 675–700.CrossRefGoogle Scholar
Reynolds, J. C. (1997) Design of the programming language Forsythe. In ALGOL-Like Languages. Springer, pp. 173–233.CrossRefGoogle Scholar
Schaefer, I., Bettini, L. & Damiani, F. (2011) Compositional type-checking for delta-oriented programming. In Proceedings of the Tenth International Conference on Aspect-Oriented Software Development, AOSD 2011. ACM, pp. 43–56.CrossRefGoogle Scholar
Schärli, N., Ducasse, S., Nierstrasz, O. & Black, A. P. (2003) Traits: Composable units of behaviour. In ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Proceedings. Springer, pp. 248–274.CrossRefGoogle Scholar
Siek, J. G. (2019) Transitivity of subtyping for intersection types. CoRR. abs/1906.09709.Google Scholar
Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Scheme and Functional Programming Workshop.Google Scholar
Siek, J. G. & Wadler, P. (2010) Threesomes, with and without blame. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM, pp. 365–376.CrossRefGoogle Scholar
Statman, R. (1985) Logical relations and the typed λ-calculus. Inf. Control. 65(2/3), 85–97.CrossRefGoogle Scholar
Statman, R. (2015) A finite model property for intersection types. Electron. Proc. Theor. Comput. Sci. 177, 1–9.CrossRefGoogle Scholar
Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198–212.CrossRefGoogle Scholar
Ungar, D. & Smith, R. B. (1988) Self: the power of simplicity (object-oriented language). In Thirty-Third IEEE Computer Society International Conference, Digest of Papers.CrossRefGoogle Scholar
Wadler, P. (1998) The expression problem. Posted on the Java Genericity Mailing List. Google Scholar
Wadler, P. & Blott, S. (1989) 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. ACM Press, pp. 60–76.CrossRefGoogle Scholar
Wadler, P. & Findler, R. B. (2009) Well-typed programs can’t be blamed. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, York, UK, March 22–29, 2009. Proceedings. Springer, pp. 1–16.CrossRefGoogle Scholar
Wand, M. (1989) Type inference for record concatenation and multiple inheritance. Proceedings. Fourth Annual Symposium on Logic in Computer Science. pp. 92–97.CrossRefGoogle Scholar
Wang, Y., Zhang, H., d. S. Oliveira, B. C. & Servetto, M. (2018) FHJ: A formal model for hierarchical dispatching and overriding. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16–21, 2018, Amsterdam, The Netherlands.Google Scholar
White, L., Bour, F. & Yallop, J. (2014) Modular implicits. In Proceedings ML Family/OCaml Users and Developers Workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4–5, 2014, pp. 22–63.Google Scholar
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94.CrossRefGoogle Scholar
Xie, N., Oliveira, B. C. d. S., Bi, X. & Schrijvers, T. (2020) Row and bounded polymorphism via disjoint polymorphism. In 34th European Conference on Object-Oriented Programming, ECOOP 2020.Google Scholar
Zwanenburg, J. (1995) Record concatenation with intersection types.Google Scholar
Zwanenburg, J. (1997) A type system for record concatenation and subtyping. Technical report. Eindhoven University of Technology.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.