Koka: Programming with Row Polymorphic Effect Types

Daan Leijen

Source-linked AI summary

Koka: Programming with Row Polymorphic Effect Types

Daan Leijen

arXiv:1406.2061v1Jun 9, 2014cs.PL

TL;DR

Conventional ML and Haskell types leave important function behaviors unspecified, including effects, exceptions, and divergence. Koka addresses this with inferred row-polymorphic effect types whose semantic guarantees support safe state encapsulation and polymorphism, and implements the approach in a language used on practical sample programs.

Problem
ML and Haskell types do not precisely describe behaviors such as side effects, exceptions, divergence, or lazy-result failures.
Method
Koka combines Hindley-Milner-style inference with row-polymorphic effect types, duplicate labels, and state effects for safe encapsulation and polymorphism.
Results
Koka fully implements the system and has been used successfully in small- to medium-sized programs, while the system proves semantic safety properties for exceptions, termination, and encapsulated state.
Takeaways & Limitations
Effect types provide a practical way to expose function behaviors and support safe reasoning about exceptions, divergence, and stateful operations.
Takeaways & Limitations
A proper monadic semantics for Koka's polymorphic effects is left for future work, and earlier subtyping-based inference could become undecidable with polymorphism.

Abstract

from arXiv · show

We propose a programming model where effects are treated in a disciplined way, and where the potential side-effects of a function are apparent in its type signature. The type and effect of expressions can also be inferred automatically, and we describe a polymorphic type inference system based on Hindley-Milner style inference. A novel feature is that we support polymorphic effects through row-polymorphism using duplicate labels. Moreover, we show that our effects are not just syntactic labels but have a deep semantic connection to the program. For example, if an expression can be typed without an exn effect, then it will never throw an unhandled exception. Similar to Haskell's `runST` we show how we can safely encapsulate stateful operations. Through the state effect, we can also safely combine state with let-polymorphism without needing either imperative type variables or a syntactic value restriction. Finally, our system is implemented fully in a new language called Koka and has been used successfully on various small to medium-sized sample programs ranging from a Markdown processor to a tier-splitted chat application. You can try out Koka live at www.rise4fun.com/koka/tutorial.

1. Introduction

Koka makes function effects explicit in types and combines row-polymorphic effect typing with semantic safety guarantees. The system supports safe polymorphic state and has been implemented successfully in practical sample programs.

1. Introduction: Koka treats effects as part of function signatures, making behaviors such as console output and exceptions explicit rather than leaving them unspecified by ordinary input-output types.Effects and expression effects are inferred automatically, reducing the need for programmer-written effect annotations.
1. Introduction: Row-polymorphic effect types allow duplicated effects, simplifying effect types and giving natural types to effect elimination forms such as exception handlers.
1. Introduction: Effect types have semantic force: expressions typed without exn never throw unhandled exceptions, while expressions typed without div always terminate.
1. Introduction: Modeling state as an effect safely combines mutable state with let-polymorphism without imperative type variables or a syntactic value restriction.The system also safely encapsulates local state and proves that references or stateful behavior cannot escape the encapsulation scope.
1. Introduction: Koka fully implements the effect system and has been used successfully in small- to medium-sized programs, including a Markdown processor and a tier-splitted chat application.

2. Overview

Koka addresses the limited behavioral precision of conventional ML and Haskell types with strict semantics and inferred effectful function types. Its row-polymorphic design avoids difficult effect-union constraints while supporting effects determined by higher-order arguments.

2. Overview: ML and Haskell types do not precisely describe behaviors such as side effects, exceptions, divergence, or lazy-result failures, motivating explicit effect information.
2. Overview: Koka uses strict semantics and function types of the form (τ1,...,τn) →ε τ, making potential side effects apparent at function application.Basic effects include total, exn, div, ndet, allocation, reading, writing, and io.
2. Overview: Rows combine effects such as exn and div into named aliases, including pure = ⟨exn, div⟩ and state aliases built from allocation, reading, and writing.
2. Overview: Effect-polymorphic functions can derive their effects from passed functions, as illustrated by map and by foo, whose effect combines its arguments with exn.
2. Overview: Effect unions create unsolved unification constraints, while earlier subtyping constraints became complex and could make inference undecidable in combination with polymorphism.
2. Overview: Koka instead uses row polymorphism with open effect rows and duplicate labels, enabling straightforward inference and a polymorphic type for foo.The approach uses rows of the form ⟨l | µ⟩ and avoids additional machinery for duplicate effects.

2.4. Duplicate effects

Koka uses row-polymorphic effect types with duplicate labels, simplifying inference and precisely typing effect elimination such as exception handling. The system also connects these effect types to encapsulated state and supports practical local-state programming.

2.4. Duplicate effects: Duplicate effect labels make row unification deterministic without lacks constraints or presence/absence flags.For ⟨exn|µ⟩ ∼ ⟨exn⟩, duplicate-label rows admit only µ = ⟨⟩.
2.4. Duplicate effects: Duplicate labels precisely type exception handlers because catching removes one exn effect while a handler may contribute another.A handler that can throw yields an effect such as ⟨exn|exn|µ′⟩.
2.4. Duplicate effects: Duplicate effects have semantic significance under a monadic interpretation, where they can represent nested exception layers.An injected exception can pass through an inner catch and be handled by an outer handler.
2.5. Heap effects: Koka safely encapsulates local mutable state by discarding st⟨h⟩ when the heap variable is absent from argument and result types.This corresponds to a runST-like operation and lets locally stateful functions such as fib be treated as total.
2.5. Heap effects: The same inference can discard local state in nontrivial programs, including the Garsia-Wachs algorithm, yielding a pure effect.The algorithm uses updateable references internally, but those effects are not observable by callers.

2.6. Heap safety

Koka uses effect typing to control polymorphism, encapsulated state, and divergence. It rejects unsound polymorphic references, proves heap encapsulation safety, and analyzes higher-order stateful divergence through heap-sensitive constraints.

2.6. Heap safety: Effect-based generalization rejects unsound polymorphic references while allowing generalization of non-stateful expressions regardless of syntax.Koka restricts generalization to total expressions and rejects the ML example because the reference has an alloc⟨h⟩ effect.
2.6. Heap safety: Koka proves that well-typed encapsulated computations cannot leak references or expose their internal state.The result covers a strict language combined with exceptions and divergence.
2.7. Divergence: Its termination checker omits divergence when recursive calls decrease inductive data or remain productive for co-inductive data.The analysis is described as limited and syntactically fragile, but usable in practice.
2.7. Divergence: Higher-order mutable state can diverge without syntactic recursion, as Landin’s knot repeatedly reads a function stored in the heap.The example updates a reference with foo itself and then calls foo.
2.7. Divergence: Heap-sensitive hdiv constraints assign divergence only when a read value’s type contains the heap and the current effect must therefore include div.This precision avoids blaming reads of non-function or non-stateful values, unlike the conservative formal-development approach.

2.8. Koka in practice

Koka implements its effect inference system and applies it to practical programs, including a Markdown processor and safe server–client tier splitting. The examples show both successful execution and automatic control of local state and cross-tier effects.

Implementation: The implemented Koka system has a JavaScript backend, runs in NodeJS or a web page, and has been tested on small to medium-sized programs.The paper reports implementation of effect inference and extensions in a freely available system.
Markdown: The Markdown processor passes the full Markdown test suite, including the document used to write the article itself.The processor parses, analyzes, collects link definitions, numbers sections, and renders inline elements.
Markdown: Almost all Markdown functions are inferred total while only a few driver functions perform effects such as reading input files.Internal functions still use local mutable structures for efficient construction.
Safe tier-splitting: Koka’s tier-splitting function uses effect types to enable safe server–client separation while exposing communication types in its signature.The type distinguishes server and client functions and returns an io effect.
Safe tier-splitting: Tier splitting addresses unsafe cross-tier calls and shared global state by tracking server/client effects and preventing non-generalized shared heaps from being discarded.State local to each handler may be discarded, but references captured from an outer scope prevent heap generalization.

3. The type system

The type system formalizes Koka’s polymorphic effects using effect rows that permit duplicate labels, with rules for functions, applications, bindings, exception handling, and state isolation. Type inference is principal, sound, and complete, while let-bound function types can be simplified and reopened safely at instantiation.

Effect rows: Effect rows are permutation-invariant and may contain duplicate labels, so ⟨exn,exn⟩ differs from ⟨exn⟩.This row structure supports polymorphic effects and gives natural types to effect-elimination forms such as catching exceptions.
Core calculus: The core calculus includes variables, primitives, applications, functions, sequencing, let bindings, exception catching, and state isolation through run.The surface syntax includes primitives for divergence, exceptions, allocation, reads, and writes.
Typing rules: Function effects move from lambda bodies into function types, while application requires the function and argument derivations to share an effect.Open effect rows make this requirement compatible with polymorphic functions such as the identity function.
Typing rules: Generalization requires a total derived effect, providing the semantic analogue of ML’s value restriction for let-polymorphism.The restriction ensures sound semantics even though effects are inferred rather than imposed syntactically.
Type inference: The system has an efficient inference algorithm that computes principal types and is sound and complete with respect to the formal typing rules.The calculus also provides dedicated rules for heap expressions and constants, including conversion of heaps into type environments.
Simplifying types: Koka closes let-bound function effects for readable types and reopens closed effects with fresh variables at instantiation, preserving soundness and potentially accepting more programs.This simplification applies only to let-bound variables; applying it to lambda-bound parameters would destroy principal type inference.

4. Semantics of effects

The semantics separates values, heaps, exceptions, and evaluation contexts, then defines reductions for ordinary computation, exception propagation, heap operations, and state isolation. Its unconventional heap representation lets run discard local state and supports a purity theorem about effect-free expressions.

Semantic model: The semantics uses explicit heap bindings, value forms, partially applied handlers and assignments, and general constants to model effectful execution.Heap values are typed under environments containing all heap bindings, and heap bindings induce the state effect st⟨h⟩.
Exceptions: Exception reductions propagate throws to the nearest handler or state boundary, while catch either passes a thrown value to its handler or returns an ordinary value unchanged.Exceptions raised by handlers continue propagating to their nearest enclosing handler.
Heap effects: Heap reductions allocate bindings, read and write references, and lift or merge heaps so operations act on the nearest enclosing heap.The evaluation contexts exclude heap bindings and run expressions when locating these operations.
State isolation: State isolation through run pushes into lambdas or partial handlers and then discards a local heap when its references cannot escape.The side condition frv(w) ∩ dom(ϕ) = ∅ preserves well-formedness by preventing references from escaping their binding.
Evaluation: Evaluation contexts enforce strict leftmost-outermost reduction, and the reflexive-transitive evaluation relation is functional despite nondeterministic heap lifting and merging order.A diamond theorem handles the unconstrained order of LIFT and MERGE reductions.
Semantic consequences: The unconventional heap model enables the purity theorem that an expression typed without st⟨h⟩ cannot evaluate to a heap-bound value.This theorem is difficult to state with a conventional externally scoped heap.

5. Semantic soundness

The system proves semantic soundness through subject reduction and untypeability of faulty expressions, including guarantees for state isolation and local references.

Semantic soundness: Well-typed programs either produce well-typed answers or diverge, because reduction preserves typing and faulty expressions are untypeable.The proof combines subject reduction with the result that faulty expressions cannot be typed.
Subject reduction: Stateful effects cannot be discarded in evaluation contexts, preventing generalization of stateful references and supporting subject reduction.This property is captured by the stateful-effects lemma and is used in the critical let-binding case.
Faulty expressions: The system rejects undefined operations, escaping reads and writes, escaping references, invalid applications, and other faulty expressions by making them untypeable.The faulty-expression definition includes violations involving undefined constants, heaps, functions, references, and exceptions.
Faulty expressions: The proof establishes soundness of run in a strict setting, including the prevention of local references and state from escaping their encapsulation scope.The authors identify escaping state as the key case and connect it to state isolation through run.

6. Effectful semantics

Effect rows have semantic force: omitting exception, state, or divergence effects constrains possible runtime outcomes, while local effects may remain encapsulated.

Exceptions: If exn is absent from an expression's effect row, evaluation cannot produce an uncaught exception result, though local catches may handle exceptions.The theorem allows divergence or ordinary values and heap-allocated values, but excludes throw results.
State: If st⟨h⟩ is absent, evaluation cannot return a heap containing that state, although stateful behavior may remain hidden inside run.The state theorem excludes heap results while explicitly allowing encapsulated state operations.
Divergence: If div is absent, evaluation is guaranteed to terminate, making the divergence effect a static termination guarantee.The divergence theorem states that evaluation reaches an answer rather than diverging.
Divergence: Logical-relations reasoning proves that well-typed terms without div belong to reducible sets preserved by reduction.The proof uses preservation of reducibility and membership of well-typed terms in the reducible interpretation.
Semantic correspondence: These theorems establish a dynamic correspondence between effect types and program behavior rather than treating effects as merely syntactic labels.The section presents semantic consequences for exceptions, state, and divergence as evidence of this correspondence.

7. Related work

The paper situates its effect system among polymorphic, monadic, privilege-based, region-based, and handler-based approaches, while identifying limitations in expressiveness and translation.

State and polymorphism: The system's polymorphic mutable state addresses the classic unsoundness of combining state with let-polymorphism without imperative variables or a syntactic value restriction.The paper contrasts its effect-based solution with the ML value restriction and related work on mutable state.
State encapsulation: Its run operation resembles region inference by delimiting a heap region, but regions are values and cannot access references across multiple regions.The comparison distinguishes the paper's state encapsulation from region-based formulations.
Row polymorphism: Compared with flag-based effect systems, row effects are less expressive for directly enforcing absence of a particular effect, requiring closed rows instead.The authors report that this limitation has not yet caused practical problems in their experience.
Monadic semantics: A proper monadic semantics for this system remains future work because polymorphic effects make the translation require dependently typed operations.The paper notes that a monadic translation is substantially involved for its particular system.
Effect handlers: Unlike algebraic effect handlers, this work models effects intrinsic to the language rather than user-defined operations handled through algebraic theories.The related-work discussion explicitly characterizes the approaches as different.

A. Type inference

The paper presents syntax-directed typing rules for automatic inference and proves that they are sound and complete with respect to the declarative system.

Type inference: The syntax-directed system determines the derivation tree from the syntax and removes explicit instantiation and generalization rules.Instantiation is handled at variable rules, while generalization is applied at let-bindings.
Soundness: Theorem 5 proves that every typing derivation from the syntax-directed rules is valid in the declarative system.This establishes soundness of the inference-oriented presentation.
Completeness: Theorem 6 proves completeness: declaratively typable expressions can be derived by the syntax-directed rules up to instantiation.The declarative type σ may be instantiated to the inferred type τ.

A.1. The type inference algorithm

The paper presents a type-and-effect inference algorithm based on syntax-directed rules, unification, and generalization. It proves that the algorithm is sound and complete with respect to the declarative system.

A.1. The type inference algorithm: The algorithm synthesizes substitutions, types, and effects from an environment and expression using natural inference rules.The judgment is written θΓ ⊢e : τ | ε, with θ, τ, and ε synthesized while Γ and e are inherited.
A.1. The type inference algorithm: It extends Hindley-Milner-style inference with unification of effect rows, including duplicate labels.Effect unification matches an effect row against an effect primitive and returns an effect tail plus a substitution.
A.1. The type inference algorithm: The inference algorithm is sound and complete with respect to the syntax-directed rules, and therefore with respect to the declarative rules.The paper states separate soundness and completeness theorems and notes that the proofs extend standard algorithm W with effect-type unification.
A.1. The type inference algorithm: The unification procedure adapts record unification with scoped labels and includes a dedicated rule for effect rows.Its termination depends on checking that the effect tail is not in the substitution domain.