Higher-Order Functions, Without Leaking Effects

The last episode fixed the direction — effects travel as capabilities, passed as values — and then pointed straight at the place the model was most likely to crack. A first-order function’s signature can list its capabilities honestly. But what about a function that takes another function?

fn map(f: ???, xs: List[T]) -> List[U]
//        ^^^ if f needs a Logger, what does map's signature become?

Two obvious answers are both wrong. Put the logger into f’s type, and it climbs into map’s signature too — now map advertises a logging capability it never uses, and every higher-order function would be contaminated by the effects of whatever it’s called with. Make f a pure T -> U instead, and you simply can’t pass a function that logs. Either the generic function stops being generic, or it stops being useful. This is the real test of an effect system: not the leaf functions, but the combinators that sit above them.

Five candidates, narrowed to two

The design notes lined up five ways to handle it, and most eliminated themselves.

Restricting higher-order functions to pure functions only was the quickest to drop — it guts map, filter, and fold of most of their use. Algebraic effect handlers, where f performs an effect and something up the stack handles it, were set aside too: they rely on implicit non-local control flow, which is exactly the kind of invisibility the whole effect system exists to remove, and they’d contradict the capability-passing decision already made. A closure capture type — annotating a closure with the effects it captured — turned out to be a re-spelling of the first surviving candidate, not a distinct one.

That left two real finalists:

• Effect-row polymorphism, as in Koka, Eff, and OCaml 5’s effects: give map a signature that is polymorphic over an effect variable, so it passes through whatever effects f has. map(fn x -> x+1) runs with an empty effect row; map(fn x -> { log(x); x }) infers the logger effect automatically. It infers completely and keeps map fully generic — at the cost of adding row types to the type system, and of every function type growing an effect annotation.
• Explicit capability arguments: keep the effect at the value level. A function that logs is really a function that takes a logger argument; the caller supplies the logger before handing the function to map, so by the time map sees it, it is an ordinary T -> U.

Letting the earlier decision decide

The two finalists are both workable and both proven somewhere. Row polymorphism in particular is the sophisticated, well-benchmarked answer, with a track record in real languages. On expressiveness alone it is the stronger option.

But the choice wasn’t made on expressiveness. It was made on consistency, because the two options differ on one axis that Mere had already taken a position on: row polymorphism puts effects on the function type; capability arguments keep effects at the value level and leave the function type as plain T -> U. The previous episode’s decision — capability passing — had already declared that in Mere, effects are values, not something encoded on a type. Row polymorphism is the opposite declaration, dressed for higher-order functions. Adopting it here would mean quietly reversing the stance taken one episode earlier, and dragging in row-type machinery the language otherwise works hard to avoid.

So Mere chose explicit capability arguments, and the mechanism is almost disappointingly plain:

let inc = fn x -> x + 1               // pure
let f   = fn x -> log_x(x, logger)    // caller fills in `logger`; f : Int -> Int

map(inc, xs)                          // map sees a plain Int -> Int
map(f,   xs)                          // and so does this — the cap is already inside

f uses a logger, but by the point it reaches map the logger has been supplied — it is a value that has already been consumed into the closure. What map receives is a plain Int -> Int, and map’s signature never changes: it stays (T -> U) -> List[T] -> List[U], handled by ordinary Hindley–Milner inference with no extension at all. The same account covers a closure that captures a logger from its surroundings (the sibling question the notes track alongside this one): its type is just Int -> Int, and the fact that it captured a capability doesn’t appear in the type, because it is exactly equivalent to a function that took the capability as an argument and had it filled in.

Building the trial to be sure

An argument from consistency is persuasive but not proof. The methodology this series keeps returning to — decide on paper, then dogfood before committing — applies here too: the surviving candidate was implemented as a small standalone trial before it went into the language. A ~330-line interpreter, sixteen tests, working through every shape the design had to survive: a pure function through map, a logging one, a closure that captures, partial application that fills the capability in, function composition where one side has an effect, nested higher-order calls. All of them ran on plain HM inference with no row types — and the type errors that should fire, for the programs that should be rejected, fired as expected. The claim “capability arguments need no type-system extension” stopped being a hope and became a thing that had been observed.

That is the point of a trial: the elegant-sounding option and the plain one both argue well on paper, and building the plain one cheaply is how you find out the plainness is real and not a hidden debt.

What it costs, and what’s deferred

Explicit capability arguments are not free of friction. The residual cost is verbosity in partial application — the caller has to fill capabilities in by hand, repeatedly, in a way row polymorphism would infer away. The design notes sketch a possible using sugar to soften it:

let f = fn x using [logger] -> { logger.info(x); x }   // sugar for the curried form

— but deliberately leave it unbuilt, on the principle of implementing the plain form first and judging whether the sugar earns its place from real use, rather than adding convenience ahead of the need for it. A recurring discipline: get the honest, verbose version working before deciding what to hide.

The effect model now survives higher-order functions, which was its hardest structural test. What it still can’t say is which kind of effect a capability carries — a parameter tells you a function can touch the database, but not whether it only reads, or also writes, nor whether the access is exclusive or safely shared. Presence is too coarse. Next: the grain of an effect — reading versus writing, exclusive versus shared, and the borrow annotations that draw those lines.