The two fixpoints, made one construct.
μ and ν are dual operators on monotone functors. μF is what you build; νG is what you observe. A Munu contract is the explicit witness of their interaction — the only place in the language where induction meets coinduction.
μ and ν are dual operators on monotone functors.
In conventional languages, μ is privileged — you write data, and ν is hacked on (a loop, a thread, a generator). Each fights a different battle with the runtime.
In Munu, both are first-class. A contract is the term-level witness that an algebra (μF → A) and a coalgebra (B → νG) agree on a boundary. The kernel never sees this; it sees only bytecode that steps when bound.
- Shape
- finite, built
- Tactic
- recursion · pattern match
- Examples
- Nat, List, AST, parse tree
- Type rule
- LUB (⊔) — joins of types
- Shape
- infinite, observed
- Tactic
- corecursion · observation
- Examples
- Stream, FSM, server, supervisor
- Type rule
- GLB (⊓) — meets of types
Everything is a contract.
Contracts are the construct that solves μ–ν at the language level. They are not coroutines wearing a hat. Each contract carries a behaviour clause — a do: that governs local failure, and a must: that is the obligation to its supervisor. The kernel steps bytecode; all supervision logic lives in source.
Local failure recovery
The do: formula compiles into the contract's own Mealy table. When the contract crashes, the coalgebra intercepts the Fail event. If the Mealy says Restart, unbound variables go TempFail and the contract restarts — it weathers the storm at its own layer.
Supervisor deadline
The must: formula feeds into the parent supervisor's Mealy table as a deadline. If a child breaches its must: clause, the supervisor fires MustBreach — the child's variables go PermFail. TempFail is local recovery. PermFail is contract violation.
// do: weathers the storm (TempFail + restart) formula permanent() { nu X. [fail(self, _)] <restart(self)> X and [_] X } // do: two strikes, then escalate formula two_strikes() { nu X. [fail(self, _)] <restart(self)> nu Y. [fail(self, _)] <restart(self)> nu Z. [fail(self, _)] false and [_] Z and [_] Y and [_] X }
Every variable is a dataflow variable.
Every variable has a 6-state lifecycle. Reads block until Bound. Demand is implicit — reading a WaitNeeded variable wakes its producer. When a contract's do: fires Restart, its unbound variables go TempFail. When a child breaches its must:, they go PermFail. No recovery.
Kernel state — two contracts, two variables
Trace
A ψ-term lattice with a 6-state FSM.
Gradual typing without an escape hatch. The checker proceeds by subsumption (⊑), never equality. GLB is ν (greatest fixpoint); LUB is μ (least fixpoint). The μ–ν duality at term level repeats at type level — same operators, same lattice.
Errors written for the LLMs, not the human.
The compiler is the first reader; the LLMs are the second; the human, when they choose to look, is the third. Every diagnostic emits a structured envelope with the failing constraint, the relevant positions in the AST, a candidate-fix vector, and the smallest counter-example that violates subsumption.
This is the language-level invariant that makes Munu an AI harness: the models never have to guess what the compiler meant — the constraint and a witness for its violation are both addressable terms.
error[E0308]: mismatched types --> src/main.uv:14:18 | 14 | let n: u64 = raw | ^^^ expected u64, found ψ | = help: add a cast
{ "code": "M.subsume.fail", "operator": "⊑", "expected": "u64", "got": "ψ", "site": "src/main.uv:14:18..14:21", "constraint": "ψ ⊑ u64", "witness": { "raw": "-3.14" }, "fixes": [ { "k": "insert_cast", "term": "raw as u64" }, { "k": "widen_target", "term": "i64" } ] }