Sound and Complete Type Inference for Closed Effect Rows.

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 run-time 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.