Sound and Complete Type Inference for Closed Effect Rows
Pages 144 - 168
Abstract
Koka is a functional programming language that has algebraic effect handlers and a row-based effect system. The row-based effect system infers types by naively applying the Hindley-Milner type inference. However, it infers effect-polymorphic types for many functions, which are hard to read by the programmers and have a negative runtime performance impact to the evidence-passing translation. In order to improve readability and runtime efficiency, we aim to infer closed effect rows when possible, and open those closed effect rows automatically at instantiation to avoid loss of typability. This paper gives a type inference algorithm with the and mechanisms. In this paper, we define a type inference algorithm with the open and close constructs.
References
[1]
Bauer A and Pretnar M Programming with algebraic effects and handlers J. Logic. Algebraic Methods Program. 2015 84 1 108-123
[2]
Convent, L., Lindley, S., McBride, C., McLaughlin, C.: Doo bee doo bee doo. J. Funct. Program. 30, e9 (2020). To appear in the special issue on algebraic effects and handlers
[3]
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: DeMillo, R.A. (ed.) Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 1982, pp. 207–212. ACM Press (1982).
[4]
Emrich, F., Lindley, S., Stolarek, J., Cheney, J., Coates, J.: FreezeML: complete and easy type inference for first-class polymorphism. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15–20 June 2020, pp. 423–437. ACM (2020).
[5]
Hillerström, D., Lindley, S.: Liberating effects with rows and handlers. In: Chapman, J., Swierstra, W. (eds.) Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, 18 September 2016, pp. 15–27. ACM (2016).
[6]
Jones MP Krieg-Brückner B A theory of qualified types ESOP ’92 1992 Heidelberg Springer 287-306
[7]
Kammar, O., Plotkin, G.D.: Algebraic foundations for effect-dependent optimisations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, New York, NY, USA, pp. 349–360. ACM (2012).
[8]
Karachalias G, Pretnar M, Saleh AH, Vanderhallen S, and Schrijvers T Explicit effect subtyping J. Funct. Program. 2020 30
[9]
Leijen, D.: Extensible records with scoped labels. In: Proceedings of the 2005 Symposium on Trends in Functional Programming, pp. 297–312 (2005)
[10]
Leijen, D.: HMF: simple type inference for first-class polymorphism. In: Proceedings of the 13th ACM Symposium of the International Conference on Functional Programming, ICFP 2008, Victoria, Canada, September 2008.
[11]
Leijen, D.: Koka: programming with row polymorphic effect types. In: 5th Workshop on Mathematically Structured Functional Programming, MSFP 2014 (2014).
[12]
Leijen, D.: 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, pp. 486–499, January 2017.
[13]
Lindley, S., McBride, C., McLaughlin, C.: Do be do be do. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, pp. 500–514, January 2017.
[14]
Jones, S.P., Washburn, G., Weirich, S.: Wobbly types: type inference for generalised algebraic data types. MS-CIS-05-26. Microsoft Research, July 2004
[15]
Plotkin GD and Power J Algebraic operations and generic effects Appl. Categ. Struct. 2003 11 1 69-94
[16]
Pretnar, M.: Inferring algebraic effects. Log. Methods Comput. Sci. 10(3) (2014).
[17]
Rémy, D.: Type inference for records in natural extension of ML. In: Theoretical Aspects of Object-Oriented Programming, pp. 67–95 (1994)
[18]
Robinson JA A machine-oriented logic based on the resolution principle J. ACM 1965 12 1 23-41
[19]
Wright AK Simple imperative polymorphism LISP Symb. Comput. 1995 8 4 343-355
[20]
Xie, N., Brachthauser, J., Hillerstrom, D., Schuster, P., Leijen, D.: Effect handlers, evidently. In: The 25th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM SIGPLAN, August 2020. https://www.microsoft.com/en-us/research/publication/effect-handlers-evidently/
[21]
Xie, N., Leijen, D.: Generized evidence passing for effect handlers - efficient compilation of effect handlers to C. In: Proceedings of the 26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021). Virtual, August 2021
Index Terms
- Sound and Complete Type Inference for Closed Effect Rows
Index terms have been assigned to the content through auto-classification.
Recommendations
Type inference with simple selftypes is NP-complete
The metavariable self is fundamental in object-oriented languages. Typing self in the presence of inheritance has been studied by Abadi and Cardelli, Bruce, and others. A key concept in these developments is the notion of selftype, which enables ...
Deriving a complete type inference for Hindley-Milner and vector sizes using expansion
Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract ...
Deriving a complete type inference for hindley-milner and vector sizes using expansion
PEPM '13: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulationType inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Mar 2022
199 pages
© Springer Nature Switzerland AG 2022.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 17 March 2022
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Feb 2025