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) = var a := 0 var b := 1 repeat(n) fn let t = a + b a := b b := t a

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 { ctl yield(Int) : Unit }

fn produce(n) : !{Gen} Unit = if n == 0 then () else yield(n) 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) = handle produce(n) with yield(v, k) => v + k(()) return r => 0

fn count(n) = handle produce(n) with yield(v, k) => 1 + k(()) 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 { ctl choose(Int) : Int, ctl reject(Unit) : Int }

fn triple(n) : !{Amb} Int = let a = choose(n) let b = choose(n) let c = choose(n) if a > 0 && b > 0 && a <= b && a * a + b * b == c * c then a * 10000 + b * 100 + c else reject(())

fn solutions(n) = handle triple(n) with choose(m, k) => flatten(map(\(i) -> k(i), range(0, m))) reject(u, k) => Nil return r => Cons(r, Nil)

fn main() = let sols = solutions(14) println(length(sols)) 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) = handle grade(n) with final ctl abort(msg) => concat("invalid: ", msg) 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 way !{Gen} spells out that it yields. There is no root Exception class to inherit from and no hierarchy to edit; a new exception is just a new label. They union structurally across calls, so a function that can abort and a function that can timeout compose into one whose row carries both. Handling one of them discharges its label and leaves the rest in the row, which means partial recovery is something the type system tracks rather than something you promise in a comment: effect Abort { ctl abort(String) : Unit } effect Timeout { ctl timeout(Int) : Unit }

-- fetch's row spells out both failures it can raise fn fetch(id) : !{Abort, Timeout} String = if id < 0 then abort("bad id") if id > 99 then timeout(id) "ok"

-- discharge Timeout with a fallback; Abort still escapes fn with_default(id) : !{

Abort} String = handle fetch(id) with final ctl timeout(_) => "cached" return r => r

The handler peels Timeout off, so with_default is left carrying exactly !{Abort}, no more and no less. Java's checked exceptions wanted to be this and could not, because they were welded to the class hierarchy instead of being an open, structural set. Generators and streams are a producer that performs emit, transformers that catch it and re-emit, and a consumer that folds. A pipeline is handlers nested around one producer, which means there is no intermediate list, by construction: srange(1, n).smap(square).skeep(even).stake(5).ssum()

Stopping early, the stake(5), is just a handler dropping a continuation once it has what it needs. Cancellation produces garbage, and that garbage is reclaimed at a statically known point with no collector involved, which is the good part we will come back to. The stream library was inspired by Haskell's pipes and conduit. Lenses are not a library anymore they are language-integrated. They are record-update paths plus the memory model. Given three nested record types, one path expression reaches arbitrarily deep and sets several fields at once: type Vec2 = Vec2 { x: Int, y: Int } type Player = Player { pos: Vec2, hp: Int } type Game = Game { player: Player, score: Int } deriving (Lens)

let g2 = { g | player.pos.x = 30, player.hp = 95, score = 110 }

That rebuilds the spine of the nested record, and when the value is uniquely owned, each rebuild reuses the cell it just took apart, so a functional update compiles to a pointer write. No optic types are allocated, nothing is composed at runtime, the path is just addresses. The entire optics ecosystem, the van Laarhoven encoding, the profunctor zoo, the operators that look like a cat walked across the keyboard, all of it collapses here into one syntax rule and a memory discipline.

And when you genuinely need to pass an accessor around, deriving (Lens) hands you score_of and with_score as ordinary functions: let g3 = with_score(g2, 200) -- score_of(g3) == 200

They are boring functions, which is the highest compliment in functional programming! Mutable state is the var from the opening. Each var desugars to a private effect with get and set operations, discharged by a handler installed at the end of its block. The state never escapes, an analysis rejects any closure that would try to smuggle it out, and the enclosing function keeps its empty row. This is the loop you would write in Python with the signature you would want in Haskell and none of the State monad plumbing in between. Failure is the most fun, because it is functional logic programming sneaking in through the effect row. An anonymous Fail effect makes "this expression might not produce a value" a thing the type system already knows how to talk about. fail() performs it, guard(cond) performs it when a check is false, and the consumers read like a wish list: let port = cfg.at_map("port") ?? cfg.at_map("https") ?? 443 let off = customer?.tier?.discount ?? 0 let bill = [item for item in sof(cart), if prices.at_map(item) > 4]

?? falls back when the left side fails. ?. chains through options and short-circuits. The comprehension guard prunes elements that fail instead of crashing. And because var is itself just handler sugar, an entire block can be transactional: transact snapshots every live variable, runs the body in a failure context, and rolls everything back if it fails, so an overdrawn account behaves as if the purchase never happened. transact balance := balance - price guard(balance >= 0) balance else 0

Five features. One underlying mechanism, viewed through a five dimensional prism. And that lovely idea is the namesake! Modern Types So far we haven't seen a lot of type signatures which is the point, most of the time you can write down quasi-Python-looking code and inference is decidable and predictable via the usual complete-and-easy Dunfield-Krishnaswami algorithm.

You annotate only where you genuinely cross into higher-rank territory, which is rare, and the algorithm meets you exactly at that boundary. A function can demand a genuinely polymorphic argument, declared with a forall on the binder, and then use it at several types in one body: fn pick(g : forall a. (a) -> a) : Int = if g(true) then g(10) else g(20)

fn main() = println(pick(\(x) -> x))

g is forced to be polymorphic, so pick may apply it to a Bool and an Int in the same breath, which is why main can only hand it the identity function and not, say, a number. A Damas-Milner core would have unified a with Bool on the first call and rejected the second; here the forall survives into the argument. Ad-hoc polymorphism is type classes, but Lean-flavored: instances are named values you can point at, not anonymous magic conjured by global search. You write given Ord(a) to ask for a dictionary. When a type has more than one instance in scope you mark one canonical, so implicit resolution is never a coin toss, and you name the other explicitly at the call site with using: instance ordDesc : Ord(Int) { fn cmp(x, y) = int_cmp(y, x) }

canonical Ord(Int) = ordInt -- two instances share the head, so name the default

sort_by_ord(xs) -- the canonical Ord(Int) sort_by_ord(xs, using ordDesc) -- this one, reversed

The instances you do not care about, you do not write. One deriving clause off a type declaration synthesizes the boring ones, and the field accessors too: type Vec2 = Vec2 { x: Int, y: Int } deriving (Eq, Ord, Show, Lens)

with_x(v, 7) -- a derived setter, and FBIP-reused when v is unique

Classes also feed pattern matching, which is the part that tends to make PL people sit up.