Effects as data

PFCL language reference · composure.systems

1.Scope

This document describes the effect model of PFCL. It does not describe a host, or the mechanism by which a host reads commands, or the set of command kinds any particular host implements. Those are properties of hosts, not of the language.

1. A function is a PFCL expression of type T₁ × ... × Tₙ → T.
2. A command is a record value with a kind field naming the effect and further fields carrying the effect's arguments.
3. A host is any program that reads command values and performs the corresponding actions. Hosts are outside the language.
4. An emission declaration is metadata on a function stating the set of command kinds the function may include in its output. The declaration is not part of the function's type.

2.The model

A PFCL function that needs to describe an effect returns a value whose shape includes command records. In the simplest case, the return type is List<Command> and the function returns a list of command records the host will read in order.

name: app.hello
type: List<String> -> List<Command>
emits: [stdout]
body: |
  \(args).
    [ {kind: "stdout", text: "hello, machine"} ]

The function performs nothing. It computes a value — a list containing one record. A host reads the list and performs the action named by the record's kind.

// executor — any language; a switch over command kinds
for (const cmd of commands)
  switch (cmd.kind) {
    case "stdout": write(cmd.text); break;
    // a host implements only the kinds its target offers
  }

The switch is the host boundary. Above the switch, the program is a composition of pure functions. Below the switch is the host's effect implementation, which is not part of PFCL.

3.Consequences

3.1Purity holds up to the host boundary

Every function in a PFCL composition is a mathematical function of its inputs. Substituting a function for its return value does not change the observable behaviour of the composition. The property holds at every level, up to the boundary at which a host reads the returned commands.

3.2Effects are values

A command is a record, not a call into a runtime. This means effects are inspectable, loggable, testable, and replayable in ways calls are not. Two independent hosts reading the same command list produce the same actions. A test host can read the list and assert on it without performing anything.

3.3Hosts are exchangeable

The contract between a function and a host is the record schema. Any program that reads records and performs actions on their kinds is a valid host. A PFCL program compiled against one host runs against any host that implements the command kinds it emits. The vocabulary is open; a host extends what it handles by extending its switch.

Nothing in the language, the runtime, or the toolchain privileges any one host. This holds because the pure step a host drives — (state, input) -> (state, List<Command>) — never changes; only the driver around it does. The same catalog entry runs unmodified under a one-shot batch runner, a folded replay over a fixed input list, a blocking interactive loop, and a full scheduled event loop, none of which share code with each other beyond the command switch itself. The host is free to be as small as reading one list and performing it once, or as elaborate as a multi-source scheduler — the function's identity and behaviour are unaffected either way. See /execution-hosts for the full driver ladder.

3.4Purity does not depend on which host is chosen

A function's purity — every property in section 3.1 — holds regardless of which host executes its commands. Swapping a batch host for an interactive one, or a Rust host for one written in another language entirely, changes nothing about the function; it changes only which program is on the other side of the switch. This is what "host" means in this document: not a runtime the function depends on, but a replaceable reader of a fixed schema.

3.5Effects are bound to what the host offers

The effects available to a function are exactly the command kinds the host implements. A function emitting a kind the host does not handle produces no effect for that kind — the host reads the command and ignores it. This is not a language-level guarantee against nonsense emissions; it is the observable consequence of a host being a switch over kinds it recognizes.

4.What this model is not

The effects-as-data model is at level 1 of the effect-typing spectrum. Its properties are the properties named above. It is not the following.

1. Not an effect system in the type-theoretic sense. The set of command kinds a function may emit is declared in metadata, not encoded in the function's type. A caller reading a function's type learns the shape of its result but not the specific kinds it may emit.
2. Not a monad. There is no bind operation on commands; the function returns a plain data structure whose shape is chosen by the function's type. Composition of functions that describe effects is composition of functions returning lists of records, not composition of monadic actions.
3. Not effect handlers. A host is not a handler in the sense of algebraic effects. The host reads a completed list of commands rather than intercepting an effect during evaluation. There is no notion of resuming a computation from within an effect.

Each of these is a different model with different properties. The effects-as-data model is chosen for its simplicity and for the exchangeability property of section 3.3; the trade is the loss of type-level effect tracking, which is described in section 5.

5.Type-level effect tracking

Type-level effect tracking — encoding the set of kinds a function may emit in its type, so that callers may reason about effects without inspecting bodies — is planned but not implemented.

The current model declares emissions as metadata attached to a definition:

emits: [stdout, storage.write]

This declaration is documentation. It is used by the host to know which switch cases to implement for a given function. The declaration is not part of the function's type. A caller reading a function's type sees the return shape but not the effect set.

A future revision will lift emissions into the type, giving callers a type-checked view of the effect set and permitting effect polymorphism. The current level-1 model is not a placeholder — it is a coherent design that yields most of the properties one wants from effect-typing without the complexity — but the type-level extension is intended.

6.Relation to totality

Purity and totality together yield the property that a function's return value is fully determined by its inputs and terminates in bounded time. The composition of the two properties is what makes a PFCL function a mathematical function in the sense used by this document.

Totality is specified separately at composure.systems/totality. The two documents are independent — purity is not a prerequisite for totality, and vice versa — but they are usually stated together because their combination is the property that matters for reasoning about behaviour.