Module row 

Effect rows — §3.2, made real.

docs/03-type-and-effect-system.md §3.2: “Every function type carries an inferred, row-polymorphic effect row … Effect polymorphism is what keeps one standard library: map : (list[a], (a -> b ! e)) -> list[b] ! e.”

Phase 1 had four atoms, declared with uses and collected by walking what a body calls. This module is the replacement: a wider atom set, row variables, and a unifier — so a row is a thing the checker solves for rather than a list the programmer maintains.

The shape of a row

A row is a set of atoms plus a set of row variables standing for “whatever else the caller’s function argument does”:

{}                      pure
{ durable }             closed
{ dom | e }             open: dom, plus whatever `e` turns out to be
{ e, f }                the union of two callers' rows

Sets, not Rémy-style scoped labels: an effect happening twice is an effect happening. That makes union — the operation inference actually performs, once per call — trivial and exact, which is the operation that has to be right. Unification is the rarer one.

Why a row can hold several variables

fn twice(f, g) = f(); g() performs e_f ∪ e_g, and there is no single variable that is their union. A row that could hold only one tail would have to force e_f = e_g, which is a lie about a program that typechecks. Holding a set of tails costs nothing and says the truth.

Structs

Row

An effect row: a set of atoms, plus row variables standing for the rest.

Enums

Ambient

Effect

An effect atom. §3.2’s list, with the one correction Phase 2 makes to it (see Effect::Nondet).

Type Aliases

RowVarId