Sound and Complete Type Inference for Closed Effect Rows (bibtex)

by Kazuki Ikemori, Youyou Cong, Hidehiko Masuhara and Daan Leijen

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 open and close mechanisms. In this paper, we define a type inference algorithm with the open and close constructs.

View PDF

Reference:

Sound and Complete Type Inference for Closed Effect Rows (Kazuki Ikemori, Youyou Cong, Hidehiko Masuhara and Daan Leijen), In Trends in Functional Programming (Swierstra, Wouter, Wu, Nicolas, eds.), Springer International Publishing, volume 13401, 2022.

Bibtex Entry:

@inproceedings{ikemori2022tfp,
  author = {Kazuki Ikemori and Youyou Cong and Hidehiko Masuhara and Daan Leijen},
  title = {Sound and Complete Type Inference for Closed Effect Rows},
  editor = {Swierstra, Wouter and Wu, Nicolas},
  booktitle = {Trends in Functional Programming},
  year = 2022,
  publisher = {Springer International Publishing},
  pages = {144--168},
  month = mar,
  doi = {10.1007/978-3-031-21314-4_8},
  series = {Lecture Notes in Computer Science},
  volume = {13401},
  date = {2022-03-17},
  year = 2022,
  pdf = {tfp2022inference.pdf},
  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 open and close mechanisms. In this paper, we define a type inference algorithm with the open and close constructs.},
  isbn = {978-3-031-21314-4},
  url = {https://trendsfp.github.io/schedule.html}
}