Prism: An Impure Functional Language With Typed Effects
June 20, 2026
Reading Mode
Wider
compilers
formal
fp
rust
Prism: An Impure Functional Language With Typed Effects
This is going to be a very nerdy post so bear with me. Here is a function. Read it the way you would read any other function, and then tell me its type.
fn fib(n) =<br>var a := 0<br>var b := 1<br>repeat(n) fn<br>let t = a + b<br>a := b<br>b := t
That is a mutable loop. There is a var, there is assignment, there is a temporary so the swap does not eat itself. It is, line for line, the fib you would write in Python after deciding that recursion was a young person's game.
Its type is Int -> Int, it is functional but in place . There is no effect type even though the function has effects, because the effects are not observable from outside the function. As far as anyone calling it is concerned, this function is pure. It mutates two variables in place and then, before the door closes behind it, sweeps up the evidence and leaves no fingerprints. And the compiler does it all for you. It's the code you would write in Python with types you get from OCaml and no monads.
This is Prism, a proof of concept functional compiler I've been working on for the last three years, built around modeling effects with modern types inspired by the intellectual lineage of OCaml 5, Haskell and Koka. The big idea of the last five or six years of functional programming is that effects are real, effects are fine, and the interesting question is not how to avoid them but how to put them in the type system and then optimize them until they cost nothing.
Effects Are Interfaces
The one idea you need is the algebraic effect handler. An effect declares operations; a handler gives them meaning. Here is a producer that yields a sequence and has no idea who is listening:
effect Gen {<br>ctl yield(Int) : Unit
fn produce(n) : !{Gen} Unit =<br>if n == 0 then<br>()<br>else<br>yield(n)<br>produce(n - 1)
The !{Gen} in the type is the function confessing, in writing, that it performs the yield operation and someone upstream had better deal with it. Now we hand the same producer to two different handlers:
fn total(n) =<br>handle produce(n) with<br>yield(v, k) => v + k(())<br>return r => 0
fn count(n) =<br>handle produce(n) with<br>yield(v, k) => 1 + k(())<br>return r => 0
The k is the continuation, the rest of the computation, reified as an ordinary value you can hold in your hand. total resumes it and adds; count resumes it and counts. A handler can ignore k entirely (that is an exception), call it once (that is state, or a generator), or call it many times. This last one is the move that makes algebraic effects more than sugar. Here a handler finds Pythagorean triples by resuming the same continuation once per candidate, which is to say it explores a whole search tree using nothing but straight-line code and a handler that says "yes, and also try the other branch":
effect Amb {<br>ctl choose(Int) : Int,<br>ctl reject(Unit) : Int
fn triple(n) : !{Amb} Int =<br>let a = choose(n)<br>let b = choose(n)<br>let c = choose(n)<br>if a > 0 && b > 0 && a b && a * a + b * b == c * c then<br>a * 10000 + b * 100 + c<br>else<br>reject(())
fn solutions(n) =<br>handle triple(n) with<br>choose(m, k) => flatten(map(\(i) -> k(i), range(0, m)))<br>reject(u, k) => Nil<br>return r => Cons(r, Nil)
fn main() =<br>let sols = solutions(14)<br>println(length(sols))<br>println(sum(sols))
choose(n) offers a value in 0..n-1 and reject() prunes a dead branch, and because the handler resumes k once for every candidate, triple reads like a function that just picks three numbers.
If you have used OCaml 5 this will feel familiar, except OCaml keeps its effects out of the types, so you find out about an unhandled one at runtime, in production, on a Friday. If you have used Haskell this will also feel familiar, except in Haskell you would be assembling a monad transformer stack, lifting each operation through every layer by hand, and explaining to a junior colleague that a monad is just a monoid in the category of endofunctors, what's the problem. Prism's effects are row polymorphic. They union structurally across calls. There is nothing to stack and nothing to lift, because there is no tower, only a set.
One Trick, Five Ways
Once effects are first class, a remarkable number of ideas from the last thirty years of language design turn out to be unified under the same mechanism:
Exceptions are a handler that throws away the continuation. A clause marked final ctl discards k, so its body's value becomes the handler's result and the rest of the computation is simply abandoned. No Result threading, no ? confetti up the call stack, just direct-style code that stops:
fn safe_grade(n) =<br>handle grade(n) with<br>final ctl abort(msg) => concat("invalid: ", msg)<br>return r => r
And because an exception is just a label in the effect row, you get extensible exceptions for free. Each distinct failure is its own operation, so the row in a function's type spells out exactly which exceptions can escape it, the...