Document Open Access Logo

A Type-Directed Operational Semantics For a Calculus with a Merge Operator

Authors Xuejing Huang , Bruno C. d. S. Oliveira

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.26.pdf
  • Filesize: 0.68 MB
  • 32 pages

Document Identifiers

Author Details

Xuejing Huang
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China

Funding

This work has been sponsored by Hong Kong Research Grant Council projects number 17210617 and 17209519.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Xuejing Huang and Bruno C. d. S. Oliveira. A Type-Directed Operational Semantics For a Calculus with a Merge Operator. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 26:1-26:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.26

Abstract

Calculi with disjoint intersection types and a merge operator provide general mechanisms that can subsume various other features. Such calculi can also encode highly dynamic forms of object composition, which capture common programming patterns in dynamically typed languages (such as JavaScript) in a fully statically typed manner. Unfortunately, unlike many other foundational calculi (such as System F, System F_{< :} or Featherweight Java), recent calculi with the merge operator lack a (direct) operational semantics with standard and expected properties such as determinism and subject-reduction. Furthermore the metatheory for such calculi can only account for terminating programs, which is a significant restriction in practice. This paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The calculus is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016). 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. To fully obtain determinism, the λ_i^{:} calculus employs a disjointness restriction proposed in Oliveira et al.’s λ_i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike λ_i and subsequent calculi where recursion is problematic. To further relate λ_i^{:} to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of λ_i^{:} is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of λ_i^{:} is complete with respect to the λ_i type system. All results have been fully formalized in the Coq theorem prover.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Polymorphism
Keywords
  • operational semantics
  • type systems
  • intersection types

Metrics

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

Supplementary Materials

References

  1. Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Peter Sestoft, editor, Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, volume 3924 of Lecture Notes in Computer Science, pages 69-83. Springer, 2006. URL: https://doi.org/10.1007/11693024_6.
  2. João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 1-28. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_1.
  3. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment 1. The journal of symbolic logic, 48(4), 1983. Google Scholar
  4. Xuan Bi and Bruno C. d. S. Oliveira. Typed first-class traits. In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, volume 109 of LIPIcs, pages 9:1-9:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.9.
  5. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The essence of nested composition. In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, volume 109 of LIPIcs, pages 22:1-22:33. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.22.
  6. Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint polymorphism for compositional programming. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 381-409. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_14.
  7. Luca Cardelli. Amber. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors, Combinators and Functional Programming Languages, Thirteenth Spring School of the LITP, Val d'Ajol, France, May 6-10, 1985, Proceedings, volume 242 of Lecture Notes in Computer Science, pages 21-47. Springer, 1985. URL: https://doi.org/10.1007/3-540-17184-3_38.
  8. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv., 17(4):471-522, 1985. URL: https://doi.org/10.1145/6041.6042.
  9. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. Inf. Comput., 117(1):115-135, 1995. URL: https://doi.org/10.1006/inco.1995.1033.
  10. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 289-302. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676991.
  11. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 5-18. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535840.
  12. Giuseppe Castagna and Zhiwu Xu. Set-theoretic foundation of parametric polymorphism and subtyping. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 94-106. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034788.
  13. Manuel M. T. Chakravarty, Gabriele Keller, and Simon L. Peyton Jones. Associated type synonyms. In Olivier Danvy and Benjamin C. Pierce, editors, Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pages 241-253. ACM, 2005. URL: https://doi.org/10.1145/1086365.1086397.
  14. Manuel M. T. Chakravarty, Gabriele Keller, Simon L. Peyton Jones, and Simon Marlow. Associated types with class. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 1-13. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040306.
  15. Craig Chambers and Weimin Chen. Efficient multiple and predicated dispatching. In Brent Hailpern, Linda M. Northrop, and A. Michael Berman, editors, Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA '99), Denver, Colorado, USA, November 1-5, 1999, pages 238-255. ACM, 1999. URL: https://doi.org/10.1145/320384.320407.
  16. Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd D. Millstein. Multijava: modular open classes and symmetric multiple dispatch for java. In Mary Beth Rosson and Doug Lea, editors, Proceedings of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 2000), Minneapolis, Minnesota, USA, October 15-19, 2000, pages 130-145. ACM, 2000. URL: https://doi.org/10.1145/353171.353181.
  17. Adriana B. Compagnoni and Healfdene Goguen. Typed operational semantics for higher-order subtyping. Inf. Comput., 184(2):242-297, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00062-2.
  18. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Math. Log. Q., 27(2-6):45-58, 1981. URL: https://doi.org/10.1002/malq.19810270205.
  19. 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: https://doi.org/10.1145/1869459.1869489.
  20. Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 364-377. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951945.
  21. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 198-208. ACM, 2000. URL: https://doi.org/10.1145/351240.351259.
  22. Dominique Devriese and Frank Piessens. On the bright side of type classes: instance arguments in agda. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 143-155. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034796.
  23. Joshua Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133-165, 2014. URL: https://doi.org/10.1017/S0956796813000270.
  24. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 250-266. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_16.
  25. Facebook. Flow. https://flow.org/, 2014.
  26. Yangyue Feng and Zhaohui Luo. Typed operational semantics for dependent record types. In Tom Hirschowitz, editor, Proceedings Types for Proofs and Programs, Revised Selected Papers, TYPES 2009, Aussois, France, 12-15th May 2009, volume 53 of EPTCS, pages 30-46, 2009. URL: https://doi.org/10.4204/EPTCS.53.3.
  27. Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In David B. MacQueen and Luca Cardelli, editors, POPL '98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998, pages 171-183. ACM, 1998. URL: https://doi.org/10.1145/268946.268961.
  28. Timothy S. Freeman and Frank Pfenning. Refinement types for ML. In David S. Wise, editor, Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268-277. ACM, 1991. URL: https://doi.org/10.1145/113445.113468.
  29. Healfdene Goguen. A typed operational semantics for type theory. PhD thesis, University of Edinburgh, UK, 1994. URL: http://hdl.handle.net/1842/405.
  30. Healfdene Goguen. Typed operational semantics. In Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin, editors, Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, volume 902 of Lecture Notes in Computer Science, pages 186-200. Springer, 1995. URL: https://doi.org/10.1007/BFb0014053.
  31. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip Wadler. Type classes in haskell. ACM Trans. Program. Lang. Syst., 18(2):109-138, 1996. URL: https://doi.org/10.1145/227699.227700.
  32. Stefan Kaes. Parametric overloading in polymorphic programming languages. In Harald Ganzinger, editor, ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings, volume 300 of Lecture Notes in Computer Science, pages 131-144. Springer, 1988. URL: https://doi.org/10.1007/3-540-19027-9_9.
  33. Zhaohui Luo. Coercive subtyping. J. Log. Comput., 9(1):105-130, 1999. URL: https://doi.org/10.1093/logcom/9.1.105.
  34. Microsoft. Typescript. https://www.typescriptlang.org/, 2012.
  35. Radu Muschevici, Alex Potanin, Ewan D. Tempero, and James Noble. Multiple dispatch in practice. In Gail E. Harris, editor, 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, pages 563-582. ACM, 2008. URL: https://doi.org/10.1145/1449764.1449808.
  36. Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview of the scala programming language. Technical report, École Polytechnique Fédérale de Lausanne, 2004. Google Scholar
  37. Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In John Williams, editor, Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, pages 135-146. ACM, 1995. URL: https://doi.org/10.1145/224164.224195.
  38. Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu. Polymorphic symmetric multiple dispatch with variance. Proc. ACM Program. Lang., 3(POPL):11:1-11:28, 2019. URL: https://doi.org/10.1145/3290324.
  39. Benjamin C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Google Scholar
  40. Gordon Plotkin. Lambda-definability and logical relations, 1973. Google Scholar
  41. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pages 561-577, 1980. Google Scholar
  42. Redhat. Ceylon. https://ceylon-lang.org/, 2011.
  43. John C Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, 1988. Google Scholar
  44. John C. Reynolds. The coherence of languages with intersection types. In Takayasu Ito and Albert R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS '91, Sendai, Japan, September 24-27, 1991, Proceedings, volume 526 of Lecture Notes in Computer Science, pages 675-700. Springer, 1991. URL: https://doi.org/10.1007/3-540-54415-1_70.
  45. John C Reynolds. Design of the programming language Forsythe. In ALGOL-like languages, pages 173-233. Springer, 1997. Google Scholar
  46. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits: Composable units of behaviour. In Luca Cardelli, editor, ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings, volume 2743 of Lecture Notes in Computer Science, pages 248-274. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45070-2_12.
  47. Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006. Google Scholar
  48. Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 365-376. ACM, 2010. URL: https://doi.org/10.1145/1706299.1706342.
  49. Richard Statman. Logical relations and the typed λ-calculus. Inf. Control., 65(2/3):85-97, 1985. URL: https://doi.org/10.1016/S0019-9958(85)80001-2.
  50. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  51. David von Oheimb and Tobias Nipkow. Machine-checking the java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 119-156. Springer, 1999. URL: https://doi.org/10.1007/3-540-48737-9_4.
  52. 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: https://doi.org/10.1145/75277.75283.
  53. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 1-16. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_1.
  54. Leo White, Frédéric Bour, and Jeremy Yallop. Modular implicits. In Oleg Kiselyov and Jacques Garrigue, editors, Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014, volume 198 of EPTCS, pages 22-63, 2014. URL: https://doi.org/10.4204/EPTCS.198.2.
  55. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact