×

Explicit effect subtyping. (English) Zbl 1482.68081

Summary: As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortunately, in our experience, implementing optimisations for Eff is overly error-prone because its core language is implicitly typed, making code transformations very fragile. To remedy this, we present an explicitly typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.

MSC:

68N18 Functional programming and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barendregt, H. (1981) The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland. · Zbl 0467.03010
[2] Bauer, A., Hofmann, M., Pretnar, M. & Yallop, J. (2016) From theory to practice of algebraic effects and handlers (dagstuhl seminar 16112). Dagstuhl Reports6(3), 44-58.
[3] Bauer, A. & Pretnar, M. (2015) Programming with algebraic effects and handlers. J. Log. Alg. Program.84(1), 108-123. · Zbl 1304.68025
[4] Bi, X., Oliveira, B. C. d. S. & 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, Millstein, T. D. (ed). LIPIcs, vol. 109. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 22:1-22:33.
[5] Breazu-Tannen, V., Coquand, T., Gunter, C. A. & Scedrov, A. (1991) Inheritance as implicit coercion. Inf. Comput.93, 172-221. · Zbl 0799.68129
[6] Chandrasekaran, S. K., Leijen, D., Pretnar, M. & Schrijvers, T. (2018). Algebraic effect handlers go mainstream (dagstuhl seminar 18172). Dagstuhl Reports8(4), 104-125.
[7] Crary, K. (2000). Typed compilation of inclusive subtyping. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. ICFP’00. NY, USA: ACM, pp. 68-81. · Zbl 1321.68144
[8] Damas, L. & Milner, R. (1982) Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’82. NY, USA: ACM, pp. 207-212.
[9] Dolan, S., White, L., Sivaramakrishnan, K. C., Yallop, J. & Madhavapeddy, A. (2015) Effective concurrency through algebraic effects. In OCaml Workshop.
[10] Fuh, Y.-C. & Mishra, P. (1990) Type inference with subtypes. Theor. Comput. Sci.73(2), 155-175. · Zbl 0701.68012
[11] Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures de larithmétique dordre supérieur. PhD thesis, Université Paris VII.
[12] Girard, J.-Y., Taylor, P. & Lafont, Y. (1989) Proofs and Types. Cambridge University. · Zbl 0671.68002
[13] Henglein, F. (1994) Dynamic typing: Syntax and proof theory. In Selected Papers of the Symposium on Fourth European Symposium on Programming. ESOP’92. Amsterdam, The Netherlands: Elsevier Science Publishers B. V., pp. 197-230. · Zbl 0809.68083
[14] Hillerström, D. & Lindley, S. (2016) Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016, Chapman, J. & Swierstra, W. (eds). ACM, pp. 15-27.
[15] Hindley, R. (1969) The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc.146, 29-60. · Zbl 0196.01501
[16] Igarashi, A., Pierce, B. C. & Wadler, P. (2001) Featherweight java: A minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst.23(3), 396-450.
[17] Jones, M. P. (1992) A theory of qualified types. In ESOP’92, 4th European Symposium on Programming, Rennes, France, February 26-28, 1992, Proceedings, Krieg-Brückner, B. (ed). Lecture Notes in Computer Science, vol. 582. Springer, pp. 287-306.
[18] Kammar, O., Lindley, S. & Oury, N. (2013) Handlers in action. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming. ICFP’14. ACM, pp. 145-158. · Zbl 1323.68126
[19] Kiselyov, O. & Sivaramakrishnan, K. C. (2016) Eff directly in OCaml. In OCaml Workshop.
[20] Leijen, D. (2014) Koka: Programming with row polymorphic effect types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014, Levy, P. & Krishnaswami, N. (eds). EPTCS, vol. 153, pp. 100-126. · Zbl 1464.68062
[21] Leijen, D. (2017) Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Castagna, G. & Gordon, A. D. (eds). ACM, pp. 486-499. · Zbl 1380.68097
[22] Lindley, S., Mcbride, C. & Mclaughlin, C. (2017) Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Castagna, G. & Gordon, A. D. (eds). ACM, pp. 500-514. · Zbl 1380.68098
[23] Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Syst. Sci.17, 348-375. · Zbl 0388.68003
[24] Mitchell, J. C. (1984) Coercion and type inference. In Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL’84. New York, NY, USA: ACM, pp. 175-185.
[25] Jr, Morris, J. H. (1969) Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology.
[26] 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, Garrigue, J., Keller, G. & Sumii, E. (eds). ACM, pp. 364-377. · Zbl 1361.68046
[27] Peyton Jones, S., Vytiniotis, D., Weirich, S. & Washburn, G. (2006) Simple unification-based type inference for GADTs. In ICFP’06. · Zbl 1321.68133
[28] Plotkin, G. D. & Power, J. (2003) Algebraic operations and generic effects. Appl. Categor. Struct.11(1), 69-94. · Zbl 1023.18006
[29] Plotkin, G. D. & Pretnar, M. (2013) Handling algebraic effects. Log. Methods Comput. Sci9(4), 1-36.Please provide page range for “Plotkin & Pretnar (2013), Pretnar (2014).” · Zbl 1314.68191
[30] Pottier, F. (2001) Simplifying subtyping constraints: A theory. Inf. Comput.170(2), 153-183. · Zbl 1005.68038
[31] Pretnar, M. (2014) Inferring algebraic effects. Log. Methods Comput. Sci.10(3), 1-43. · Zbl 1341.68024
[32] Pretnar, M. (2015) An introduction to algebraic effects and handlers, invited tutorial. Electron. Notes Theor. Comput. Sci.319, 19-35. · Zbl 1351.68079
[33] Pretnar, M., Saleh, A. H., Faes, A. & Schrijvers, T. (2017) Efficient Compilation of Algebraic Effects and Handlers. Technical report. CW 708. KU Leuven Department of Computer Science.
[34] Reynolds, J. C. (1974) Towards a theory of type structure. In Programming Symposium, Proceedings Colloque Sur La Programmation. London, UK: Springer-Verlag, pp. 408-423. · Zbl 0309.68016
[35] Reynolds, J. C. (1983) Types, abstraction, and parametric polymorphism. In Information Processing, Mason, R.E.A. (ed), vol. 83, pp. 513-523.
[36] Saleh, A. H., Karachalias, G., Pretnar, M. & Schrijvers, T. (2018) Explicit effect subtyping. In ESOP. Lecture Notes in Computer Science, vol. 10801. Springer, pp. 327-354. · Zbl 1418.68065
[37] Schrijvers, T., Peyton Jones, S., Chakravarty, M. & Sulzmann, M. (2008) Type checking with open type functions. In ICFP’08. ACM, pp. 51-62. · Zbl 1323.68156
[38] Simonet, V. (2003) Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. In Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings, Ohori, A. (ed), pp. 283-302. Springer.
[39] Sulzmann, M., Chakravarty, M. M. T., Peyton Jones, S. & Donnelly, K. (2007) System F with type equality coercions. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. TLDI’07. New York, NY, USA: ACM, pp. 53-66.
[40] Traytel, D., Berghofer, S. & Nipkow, T. (2011) Extending hindley-milner type inference with coercive structural subtyping. In Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings, Yang, H. (ed). Lecture Notes in Computer Science, vol. 7078. Springer, pp. 89-104. · Zbl 1232.68012
[41] Wansbrough, K. & Peyton Jones, S. L. (1999) Once upon a polymorphic type. In POPL. ACM, pp. 15-28.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.