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

# Prism：一种带有类型化效应的不纯函数式语言 来源：https://www.stephendiehl.com/posts/prism/ 这将是一篇非常技术性的帖子，请多多包涵。这里有一个函数。像阅读其他函数一样阅读它，然后告诉我它的类型。 `` fn fib(n) = var a := 0 var b := 1 repeat(n) fn let t = a + b a := b b := t a `` 这是一个可变的循环。有`var`，有赋值，有一个临时变量来防止交换把自己吃掉。它逐行对应的是你决定递归是年轻人的游戏后在Python里写出的那个`fib`。 它的类型是`Int -> Int`，它是**函数式的，但在原地执行**。没有效果类型，尽管函数有效果，因为这些效果在函数外部是无法观察到的。对于任何调用它的人来说，这个函数是纯的。它在原地修改两个变量，然后在关门之前打扫干净证据，不留任何指纹。而编译器为你完成了这一切。这是你在Python中会写的代码，但类型来自OCaml，而且没有单子。 这就是Prism（https://github.com/sdiehl/prism），一个概念验证的函数式编译器，我已经开发了三年。它基于现代类型来建模效果，灵感来源于OCaml 5、Haskell和Koka的学术脉络。过去五六年函数式编程的一个大想法是：效果是真实的，效果没问题，有趣的问题不是如何避免它们，而是如何将它们放入类型系统，然后优化它们直到它们不耗费任何成本。 ## 效果即接口 你需要的一个概念是代数效应处理器。一个效果声明操作；一个处理器赋予它们意义。下面是一个生成序列的生产者，它不知道谁在监听： `` effect Gen { ctl yield(Int) : Unit } fn produce(n) : !{Gen} Unit = if n == 0 then () else yield(n) produce(n - 1) `` 类型中的`!{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 `` `k`是延续，即计算的剩余部分，被具体化为一个可以握在手中的普通值。`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) fn main() = let sols = solutions(14) println(length(sols)) println(sum(sols)) `` `choose(n)`提供一个在`0..n-1`范围内的值，`reject()`剪掉一个死分支，因为处理器为每个候选值恢复一次`k`，所以`triple`读起来就像一个只是选了三个数的函数。 如果你用过OCaml 5，这可能会感觉很熟悉，只不过OCaml将效果排除在类型之外，所以你会在运行时、生产环境中、一个周五发现未处理的效果。如果你用过Haskell，这也会感觉很熟悉，只不过在Haskell中你需要组装一个单子变换器栈，手工将每个操作提升通过每一层，并向一位初级同事解释单子不过是自函子范畴中的幺半群，这有什么问题。Prism的效果是行多态的。它们在调用之间以结构方式联合。没有什么需要堆叠，也没有什么需要提升，因为没有塔，只有一个集合。 ## 一个技巧，五种用法 一旦效果成为一等公民，过去三十年语言设计中大量引人注目的想法就被统一到同一个机制之下： **异常**是丢弃延续的处理器。标记为`final ctl`的子句丢弃`k`，因此其主体的值成为处理器的结果，计算的其余部分被简单地抛弃。没有`Result`的线程化，没有`?`在调用栈上撒满纸屑，只有直接风格、停止的代码： `` fn safe_grade(n) = handle grade(n) with final ctl abort(msg) => concat("invalid: ", msg) return r => r `` 由于异常只是效果行中的一个标签，你就能免费获得可扩展的异常。每个不同的失败都是它自己的操作，因此函数类型中的行精确地标明了哪些异常可能从该函数逃逸，就像`!{Gen}`标明它会生成一样。没有根`Exception`类需要继承，也没有层次结构需要编辑；一个新的异常就是一个新的标签。它们在调用之间以结构方式联合，因此一个可以`abort`的函数和一个可以`timeout`的函数组合成一个行中同时携带两者的函数。处理其中一个会释放它的标签，并将剩下的留在行中，这意味着部分恢复是类型系统跟踪的东西，而不是你在注释中承诺的东西： `` effect Abort { ctl abort(String) : Unit } effect Timeout { ctl timeout(Int) : Unit } -- fetch 的行标明了它可能引发的两种失败 fn fetch(id) : !{Abort, Timeout} String = if id < 0 then abort("bad id") if id > 99 then timeout(id) "ok" -- 用回退值处理 Timeout；Abort 仍然逃逸 fn with_default(id) : !{Abort} String = handle fetch(id) with final ctl timeout(_) => "cached" return r => r `` 处理器剥离了`Timeout`，因此`with_default`恰好携带`!{Abort}`，不多不少。Java的受检异常本想像这样，却做不到，因为它们被焊接在类层次结构上，而不是一个开放的结构化集合。 **生成器和流**是一个执行`emit`的生产者、捕获它并重新发射的变换器，以及一个折叠的消费者。一个管道是围绕一个生产者嵌套的处理器，这意味着没有中间列表，这是结构上的： `` srange(1, n).smap(square).skeep(even).stake(5).ssum() `` 提前停止——`stake(5)`——只是一个处理器在得到所需内容后丢弃延续。取消会产生垃圾，而垃圾在静态已知的点被回收，无需涉及垃圾收集器，这是我们稍后会回来看的好部分。流库的灵感来自Haskell的pipes（https://hackage.haskell.org/package/pipes）和conduit（https://hackage.haskell.org/package/conduit）。 **透镜**不再是一个库，它们被集成到语言中。它们是记录更新路径加上内存模型。给定三个嵌套的记录类型，一个路径表达式可以深入到任意深度并同时设置多个字段： `` 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 } `` 这会重建嵌套记录的脊柱，当该值是唯一拥有时，每次重建都会重用刚刚拆解开的单元，因此函数式更新编译成一个指针写入。没有分配光学类型，没有在运行时组合任何东西，路径只是地址。整个光学生态系统——van Laarhoven编码、profunctor动物园、看起来像猫走过键盘的操作符——所有这一切在这里都简化为一条语法规则和一个内存纪律。当你真正需要传递一个访问器时，`deriving (Lens)`会为你提供`score_of`和`with_score`作为普通函数： `` let g3 = with_score(g2, 200) -- score_of(g3) == 200 `` 它们是普通的函数，这是函数式编程中最高级的赞美！ **可变状态**是开头的`var`。每个`var`脱糖为一个私有效果，带有`get`和`set`操作，由其块末尾安装的处理器处理。状态永远不会逃逸，分析会拒绝任何试图将其走私出去的闭包，并且外围函数保持其空行。这是你在Python中会写的循环，带有你在Haskell中想要签名，并且没有`State`单子的管道。 **失败**是最有趣的，因为它是通过效果行偷偷溜进来的函数式逻辑编程。一个匿名的`Fail`效果使“这个表达式可能不会产生值”成为类型系统已经知道如何描述的东西。`fail()`执行它，`guard(cond)`在检查失败时执行它，而消费者读起来就像一个愿望清单： `` 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] `` `??`在左侧失败时回退。`?.`通过可选链短路。推导式过滤器在元素失败时将其修剪掉，而不是崩溃。由于`var`本身只是处理器的语法糖，整个块可以是事务性的：`transact`快照所有活跃变量，在失败上下文中运行主体，如果失败则回滚所有内容，因此透支的账户表现得好像购买从未发生过。 `` transact balance := balance - price guard(balance >= 0) balance else 0 `` 五个特性。一个底层机制，通过一个五维棱镜来观察。这个可爱的想法就是它的名字！ ## 现代类型 到目前为止，我们没有看到很多类型签名，这正是关键——大多数时候你可以写出类似Python的代码，而推理通过通常的完全且易于处理的Dunfield-Krishnaswami算法是可判定的且可预测的。你只在真正进入高阶领域的地方进行注解，这很少见，而算法正好在那个边界与你会合。一个函数可以要求一个真正多态的实参，在绑定器上用`forall`声明，然后在一个主体中以多种类型使用它： `` fn pick(g : forall a. (a) -> a) : Int = if g(true) then g(10) else g(20) fn main() = println(pick(\(x) -> x)) `` `g`被迫是多态的，因此`pick`可以在同一口气中将之应用于`Bool`和`Int`，这就是为什么`main`只能给它恒等函数，而不能给一个数字。一个Damas-Milner核心会在第一次调用时将`a`与`Bool`统一，并拒绝第二次调用；在这里`forall`存活到了参数中。 特设多态是类型类，但采用Lean风格：实例是命名值，而不是由全局一致性解析的匿名魔法。你写`given Ord(a)`来请求一个字典，你可以在调用点精确命名你想要的那个（当多个在作用域中时）： `` instance ordDesc : Ord(Int) { fn cmp(x, y) = int_cmp(y, x) } sort_by_ord(xs) -- 默认的 Ord(Int) sort_by_ord[ordDesc](xs) -- 这个，反转的 `` 你不关心的实例，你就不用写。在类型声明后加一个`deriving`子句就能合成那些无聊的实例，还有字段访问器： `` type Vec2 = Vec2 { x: Int, y: Int } deriving (Eq, Ord, Show, Lens) with_x(v, 7) -- 一个派生的设置器，当 v 唯一时会被回原地重用 `` 类也喂养模式匹配，这是让PL人们坐直的部分。一个`pattern`可以将一个类方法命名为其视图，然后那个模式就可以反构造每个有该实例的类型，通过字典分派，就像方法调用一样： `` pattern First(n) for Peek = view peek fn head_or(x : c, d : Int) : Int given Peek(c) = match x of First(n) => n _ => d `` `First(n)`匹配一个`Box`、一个`Range`，或任何其他实现了`Peek`的东西，而`head_or`同时泛化于所有这些之上。模式与包围它的函数一样多态。 某些特设多态甚至不需要类。`show`是类型导向的：编译器推断其参数的静态类型，并从实际的构造器名称合成一个结构化的打印器，递归进入字段，无需编写任何实例，也无需运行时类型分派（打印器从静态类型单态化，因此它从不读取运行时标签来决定如何打印）： `` show(42) -- "42" show([1, 2, 3]) -- "[1, 2, 3]" show((7, false)) -- "(7, false)" show(Node(Leaf, 1, Leaf)) -- "Node(Leaf, 1, Leaf)" `` 第三个轴是这篇文章真正要讲的：使效果可组合的同一个行变量也使它们多态。下面是一个高阶函数，它调用其参数两次并将结果相加。参数的效果行是一个变量`e`，也就是说`twice`不关心`f`做了什么，只关心它返回一个`Int`： `` fn twice(f : (Unit) -> Int ! {| e}) = f(()) + f(()) `` `{| e}`是“这个行，以及任何其他东西”。每个调用点将`e`与传入的thunk的实际行统一，这就是整个技巧：一个定义服务于纯参数、有效果的参数、以及完全不同效果的有效果参数，无需重载也无需包装。 `` fn pure_use() = twice() fn(u) 21 `` 这里`e`与空行`{}`统一。没有执行任何效果，因此不需要处理器，结果就是`42`。现在迫使同一个`twice`携带一个效果： `` fn tick_use() = handle twice(\(u) -> tick(())) with tick(u, k) => \(n) -> k(n)(n + 1) return r => \(n) -> r `` thunk执行`Tick`，因此`e`与`{Tick}`统一，周围的`handle`正好处理那一个标签。换成一个执行`Say`的thunk，`e`就变成`{Say}`；`twice`本身从未改变。一个处理器只命名它想要的标签，而`e`悄悄地携带所有其他东西，这就是让这些函数无需一个变换器栈来线程它们的原因。 同样的机制，三次：一个定义，抽象于类型、字典和效果之上。 ## 零成本抽象 此时，愤世嫉俗的仇恨读者（你好，Hacker News！）正在思考大多数业余围观类型对于优雅抽象的想法，即：当然，但它实际花费多少？代数效果有一个名声。教科书实现将你的整个计算具体化为一个自由单子，一棵“这是一个操作，这里是一个如何处理其结果的函数”的树，然后一个解释器遍历这棵树，在每个操作处分配一个小单元。它很漂亮，但每次`yield`都要进行一次堆分配。 Prism在重要的路径上不这样做。快速路径是Koka谱系中的证据传递，我在关键处注明了我的偏离：不是具体化计算并去找处理器，而是将活跃的处理器子句作为一个普通参数携带到每个操作点。一个`do op`变成了直接调用。所以我们不需要树、解释器循环或单元。唯一的分配是在你安装处理器时为每个处理器分配一个闭包，这是O(处理器数)，而不是O(操作数)。你可以在一个处理器下执行`yield`十亿次，而该处理器只分配了一次。 自由单子仍然在建筑中，因为某些模式确实需要它（逃逸到数据结构中的计算、真正多拍的恢复、掩码处理器）。但它是后备方案，而不是默认方案，编译器会证明你处于哪种情况。 现在将这一点应用于前面的流管道： `` for n in srange(1, 11).smap(square).skeep(even) do print(n) `` 一个过程间流分析