Prism: An Impure Functional Language With Typed Effects

Prism：一种带有类型化效应的非纯函数式语言

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. 这是一个可变循环。这里有变量（var）、赋值操作，还有一个临时变量，以确保交换过程不会覆盖自身。逐行来看，这就是你在决定“递归是年轻人的游戏”之后，在 Python 中会写出的斐波那契函数。它的类型是 Int -> Int，它是函数式的，但却是原地（in-place）执行的。尽管该函数具有副作用，但并没有副作用类型，因为这些副作用在函数外部是不可见的。对于任何调用它的人来说，这个函数是纯的。它在原地修改了两个变量，然后在函数结束前清理了现场，不留任何痕迹。这一切都由编译器为你完成。

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. 这就是 Prism，一个我过去三年一直在开发的函数式编译器概念验证项目。它围绕着利用现代类型系统对副作用进行建模，灵感来源于 OCaml 5、Haskell 和 Koka 的思想传承。过去五六年函数式编程领域的核心理念是：副作用是客观存在的，也是合理的；真正有趣的问题不是如何避免副作用，而是如何将其纳入类型系统，并对其进行优化，直到其开销降为零。

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: 你需要掌握的核心概念是“代数效应处理器”（algebraic effect handler）。效应声明操作，而处理器赋予这些操作意义。下面是一个生成序列的生产者，它完全不知道谁在监听：

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: 类型中的 !{Gen} 是该函数在“书面”上坦白：它执行了 yield 操作，上游调用者最好处理它。现在，我们将同一个生产者交给两个不同的处理器：

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”: k 是延续（continuation），即计算的剩余部分，它被具体化为一个你可以直接操作的普通值。total 恢复它并进行累加；count 恢复它并进行计数。处理器可以完全忽略 k（这就是异常），调用它一次（这就是状态或生成器），或者调用它多次。最后一种用法使得代数效应不仅仅是语法糖。在这里，处理器通过为每个候选者恢复一次相同的延续来寻找勾股数，这意味着它仅使用线性代码和一个表示“是的，同时也尝试另一个分支”的处理器，就探索了整个搜索树：

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)

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. choose(n) 提供 0 到 n-1 之间的值，而 reject() 则剪掉无效分支。由于处理器为每个候选者恢复一次 k，triple 读起来就像一个简单的挑选三个数字的函数。如果你用过 OCaml 5，这会让你感到亲切，但 OCaml 将副作用排除在类型之外，所以你往往会在周五的生产环境中才发现未处理的异常。如果你用过 Haskell，这也会让你感到熟悉，但在 Haskell 中，你必须构建一个单子转换器栈（monad transformer stack），手动将每个操作提升（lift）到每一层，并向初级同事解释“单子不过是自函子范畴上的幺半群，这有什么问题吗”。

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. Prism 的副作用是行多态（row polymorphic）的。它们在调用之间进行结构性合并。这里没有需要堆叠的东西，也没有需要提升的东西，因为这里没有“塔”，只有“集合”。