Document Open Access Logo

Dependent Merges and First-Class Environments

Authors Jinhao Tan, Bruno C. d. S. Oliveira

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2023.34.pdf
  • Filesize: 1.03 MB
  • 32 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • First-class Environments
  • Disjointness
  • Intersection Types

Metrics

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

Abstract

In most programming languages a (runtime) environment stores all the definitions that are available to programmers. Typically, environments are a meta-level notion, used only conceptually or internally in the implementation of programming languages. Only a few programming languages allow environments to be first-class values, which can be manipulated directly in programs. Although there is some research on calculi with first-class environments for statically typed programming languages, these calculi typically have significant restrictions.
In this paper we propose a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them. Such operators include: reification of the current environment, environment concatenation, environment restriction, and reflection mechanisms for running computations under a given environment. In 𝖤_i any type can act as a context (i.e. an environment type) and contexts are simply types. Furthermore, because 𝖤_i supports subtyping, there is a natural notion of context subtyping. There are two important ideas in 𝖤_i that generalize and are inspired by existing notions in the literature. The 𝖤_i calculus borrows disjoint intersection types and a merge operator, used in 𝖤_i to model contexts and environments, from the λ_i calculus. However, unlike the merges in λ_i, the merges in 𝖤_i can depend on previous components of a merge. From implicit calculi, the 𝖤_i calculus borrows the notion of a query, which allows type-based lookups on environments. In particular, queries are key to the ability of 𝖤_i to reify the current environment, or some parts of it. We prove the determinism and type soundness of 𝖤_i, and show that 𝖤_i can encode all well-typed λ_i programs.

Cite As Get BibTex

Jinhao Tan and Bruno C. d. S. Oliveira. Dependent Merges and First-Class Environments. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 34:1-34:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.34

Author Details

Jinhao Tan
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China

Funding

Hong Kong Research Grant Council projects number 17209520 and 17209821 sponsored this work.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Supplementary Materials

References

  1. Martin Abadi, Luca Cardelli, P-L Curien, and J-J Lévy. Explicit substitutions. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 31-46, 1989. 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. Henk Barendregt. Introduction to generalized type systems. J. Funct. Program., 1(2):125-154, 1991. URL: https://doi.org/10.1017/s0956796800020025.
  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. Luca Cardelli. Program fragments, linking, and modularization. In Peter Lee, Fritz Henglein, and Neil D. Jones, editors, Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, pages 266-277. ACM Press, 1997. URL: https://doi.org/10.1145/263699.263735.
  8. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In Conference on LISP and Functional Programming, 1992. Google Scholar
  9. Coq development team. The coq proof assistant. URL: http://coq.inria.fr/.
  10. Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine. Sci. Comput. Program., 8(2):173-202, 1987. URL: https://doi.org/10.1016/0167-6423(87)90020-7.
  11. 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.
  12. Bruno C. d. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi. The implicit calculus: a new foundation for generic programming. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, pages 35-44. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254070.
  13. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming (ICFP), 2000. Google Scholar
  14. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001. URL: https://doi.org/10.1145/382780.382785.
  15. Jana Dunfield. Elaborating intersection and union types. Journal of Functional Programming (JFP), 24(2-3):133-165, 2014. Google Scholar
  16. Matthias Felleisen and Daniel P. Friedman. A calculus for assignments in higher-order languages. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987, pages 314-325. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41654.
  17. Olivier Flückiger, Guido Chari, Jan Ječmen, Ming-Ho Yee, Jakob Hain, and Jan Vitek. R melts brains: An ir for first-class environments and lazy effectful arguments. In Proceedings of the 15th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2019, pages 55-66. Association for Computing Machinery, 2019. Google Scholar
  18. David Gelernter, Suresh Jagannathan, and Thomas London. Environments as first class objects. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987, pages 98-110. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41634.
  19. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 123-137, 1994. Google Scholar
  20. Robert Harper and John C. Mitchell. On the type structure of standard ML. ACM Trans. Program. Lang. Syst., 15(2):211-252, 1993. URL: https://doi.org/10.1145/169701.169696.
  21. 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: https://doi.org/10.4230/LIPIcs.ECOOP.2020.26.
  22. Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. Taming the merge operator. Journal of Functional Programming, 31:e28, 2021. URL: https://doi.org/10.1017/S0956796821000186.
  23. Suresh Jagannathan. Dynamic modules in higher-order languages. In Henri E. Bal, editor, Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages, May 16-19, 1994, Toulouse, France, pages 74-87. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/ICCL.1994.288391.
  24. Suresh Jagannathan. Metalevel building blocks for modular systems. ACM Trans. Program. Lang. Syst., 16(3):456-492, 1994. URL: https://doi.org/10.1145/177492.177578.
  25. P. J. Landin. The mechanical evaluation of expressions. Comput. J., 6(4):308-320, 1964. URL: https://doi.org/10.1093/comjnl/6.4.308.
  26. Shinn-Der Lee and Daniel P. Friedman. Quasi-static scoping: Sharing variable bindings across multiple lexical scopes. In Mary S. Van Deusen and Bernard Lang, editors, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, pages 479-492. ACM Press, 1993. URL: https://doi.org/10.1145/158511.158706.
  27. David B. MacQueen. Modules for standard ML. In Robert S. Boyer, Edward S. Schneider, and Guy L. Steele Jr., editors, Proceedings of the 1984 ACM Conference on LISP and Functional Programming, LFP 1984, Austin, Texas, USA, August 5-8, 1984, pages 198-207. ACM, 1984. URL: https://doi.org/10.1145/800055.802036.
  28. Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias. Resolution as intersection subtyping via modus ponens. Proc. ACM Program. Lang., 4(OOPSLA):206:1-206:30, 2020. URL: https://doi.org/10.1145/3428274.
  29. James S. Miller and Guillermo Juan Rozas. Free variables and first-class environments. LISP Symb. Comput., 4(2):107-141, 1991. Google Scholar
  30. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic (TOCL), 9(3):1-49, 2008. Google Scholar
  31. 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), 2017. Google Scholar
  32. Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In International Conference on Functional Programming (ICFP), 2016. Google Scholar
  33. Benjamin C Pierce. Programming with intersection types and bounded polymorphism. PhD thesis, University of Pennsylvania, 1991. Google Scholar
  34. 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
  35. Dag Prawitz. Natural deduction: A proof-theoretical study. Courier Dover Publications, 2006. Google Scholar
  36. Christian Queinnec and David De Roure. Sharing code through first-class environments. In Robert Harper and Richard L. Wexelblat, editors, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996, pages 251-261. ACM, 1996. URL: https://doi.org/10.1145/232627.232653.
  37. Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. Union Types with Disjoint Switches. In 36th European Conference on Object-Oriented Programming (ECOOP 2022), Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:31, 2022. Google Scholar
  38. John C Reynolds. Preliminary design of the programming language forsythe. Technical report, Carnegie Mellon University, 1988. Google Scholar
  39. 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
  40. John C Reynolds. Design of the programming language forsythe. In ALGOL-like languages, pages 173-233. Birkhauser Boston Inc., 1997. Google Scholar
  41. Andreas Rossberg. 1ml - core and modules united. J. Funct. Program., 28:e22, 2018. URL: https://doi.org/10.1017/S0956796818000205.
  42. Andreas Rossberg, Claudio Russo, and Derek Dreyer. F-ing modules. Journal of functional programming, 24(5):529-607, 2014. Google Scholar
  43. Arjen Rouvoet. Programs for free: Towards the formalization of implicit resolution in scala. Master’s thesis, TU Delft, 2016. Google Scholar
  44. Masahiko Sato, Takafumi Sakurai, and Rod M. Burstall. Explicit environments. Fundam. Informaticae, 45(1-2):79-115, 2001. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi45-1-2-05.
  45. Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama. A simply typed context calculus with first-class environments. J. Funct. Log. Program., 2002, 2002. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/2002/S02-01/JFLP-A02-04.pdf.
  46. Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. COCHIS: stable and coherent implicits. J. Funct. Program., 29:e3, 2019. URL: https://doi.org/10.1017/S0956796818000242.
  47. Shin-ya Nishizaki. Simply typed lambda calculus with first-class environments. Publications of the Research Institute for Mathematical Sciences, 30(6):1055-1121, 1994. Google Scholar
  48. Christopher A Stone and Robert Harper. Extensional equivalence and singleton types. ACM Transactions on Computational Logic (TOCL), 7(4):676-722, 2006. Google Scholar
  49. Philip Wadler. The expression problem. Java-genericity mailing list, 1998. Google Scholar
  50. Philip Wadler. Propositions as types. Commun. ACM, 58(12):75-84, 2015. URL: https://doi.org/10.1145/2699407.
  51. 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
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact