写的时候听的歌:
我很早之前就知道了 Algebraic Effect 这么一个东西,但是长久以来一直都没有了解过他的理论,最近把存了很久但是没读的 Andrej Bauer 写的 What is algebraic about algebraic effects and handlers 拿出来读一下,打算写一系列文章记录自己的理解,秉着由浅入深的观念,第一篇文章我们就讲一下在工程学上,代数效应是什么,能干什么。
我相当不喜欢把 Algebraic effect 翻译成代数效应,从其本质上来讲,“关于副作用的代数理论”才是更合适的名字,但是这显然无助于本节的理解。
什么是工程上的代数效应?
在软件工程上的代数效应可以用 java 的 checked exception 作为引入,没错,就是那些必须要写在方法签名里的异常,例如,如果你有一个抛出 IOException 的函数,那么你必须在签名里添加上 throws IOException:
public static void foo() throws IOException {
throw new IOException();
}
这个 throws 起到了对这个函数进行“着色”的作用,任何对 foo 函数的调用要么需要立刻处理这个异常,要么同样需要在自己的签名上添加 throws IOException。在上面的例子中,一个很重要的地方是 throw new IOException() 语句实际上是一个副作用:它与 foo 原本的计算过程没有任何关系,也就是说,这里的 foo 不是一个纯函数。试想一下,假设 foo 没有函数签名上的 throws 标记,那么在调用 foo 的时候无法确定它会给出想要的结果,还是会抛出一个异常,这正对应了“副作用”一词的含义。
代数效应相比起一个简陋的 checked exception 而言主要多了如下两点
- “副作用”不仅仅局限在异常上,任何能使函数不纯的广义副作用都可以用一个类似
throw的运算来触发,同时函数的签名会记录所有这些副作用的种类,将其算作类型系统的一部分。 - 在 java 以及拥有类似异常机制的一系列语言中,我们可以使用
try-catch块来对异常进行处理,而对于代数效应来说,我们用一个专门的 handler 来替换try-catch块,handler 的用法类似一个switch语句,我们可以在其中判断哪一个副作用被触发了,从而执行对应的逻辑(类比try-catch中的catch块可以处理多种不同的异常。不仅如此,try-catch块只能做到在异常抛出后进行一些所谓的 "clean up" 逻辑,而不能回到异常抛出的现场继续执行代码,也就是说,在下面的代码中try { int a = 1; int b = 0; int c = a / b; System.out.println("Hello World"); } catch (ArithmeticException e) { System.out.println("Division by zero!"); }我们是如何也不可能在异常抛出后回到抛出异常的地方去“恢复(recover)”代码的执行。而在代数效应中,handler 将代码分成了两个世界:触发副作用时,会将当前的世界暂停,切换到 handler 的世界中处理这个副作用,而当处理结束后,则会切换回触发副作用的那个世界继续执行。
我们可以用伪代码来解释一下上面的两个例子,对于第一条来说,我们需要先了解副作用是什么,副作用直觉上来说是任何和函数的返回值无关的语句,比如在如下的函数中
public static int bar() {
System.out.println("baz");
return 114514;
}
那一行的 print 语句就是这个函数的副作用,因为它的存在并不影响函数的返回值,同理,诸如日志记录等一般在一个函数中也算如副作用的范畴。现在,让我们换一种方式,我们可以创造一种特殊的结构来代表一种副作用,例如
effect void PrintEffect(content: String);
effect void LogEffect(content: String);
分别对应了打印和记录日志两种副作用,这样,在原本程序中我们直接调用 System.out.println 的地方,我们都切换成 perform print() 语句,例如,上面的 bar 函数会变成
public static int bar() {
perform PrintEffect("baz");
return 114514;
}
要理解这些变化,请切记时时都要和 java 的 checked exception 做对比,诸如上面对于两种副作用的定义,就可以类比 java 中对异常的定义,而 perform 则像是一个更通用的 throw,通过这种对应,我们对这些改变就不会那么一头雾水,不仅如此,如果你仔细思考,应该不难发现我们还缺了点什么,没错,就是函数签名上的标记,对于 checked exception,我们要在函数签名上加上 throws,那么这次,让我们也在函数签名上加上一个标记
public static int bar() effectful PrintEffect {
perform PrintEffect("baz");
return 114514;
}
现在,如果合理的类比 checked exception 的话,读者应该立刻对其中我们创造出来的新内容感到熟悉。在完成这一部分内容之后,我们需要类比 try-catch 语句来设计 handler,在调用 bar 的时候,我们可以使用如下的语法:
int result = handle {
bar();
} with (PrintEffect(var str)) {
System.out.println(str);
resume;
}
在调用 bar 时,函数执行到 perform PrintEffect("baz"),就会跳出函数内部,来到外部的 with 块中,执行真正的 println 语句,而执行完毕后,resume 会将控制流重新交回函数内部,函数继续 perform 之后的部分开始执行语句 return 114514;,因此,我们的 handle-with 块是具有返回值的,这也体现在我们将返回值赋给 result 这一点上。
代数效应有什么工程价值?
那么,代数效应这么一个看上去是 pro max 版 checked exception 的东西,到底有什么工程价值呢?如果读者曾经写过异步代码,想必对 async/await 不陌生,而 async/await 的底层实现正依赖于与上面的介绍极为接近的过程,我们需要首先在 await 的位置将程序挂起,“进入”到被 await 语句的世界中,接着从被 await 的语句的世界中返回病恢复当前控制流的执行,因此,如果我们的语言拥有代数效用,那么就可以直接在语言层面直接立刻实现基于 async/await 的异步,以如下伪代码为例:
public static int asyncFunc() effectful YieldEffect {
perform YieldEffect(() -> expensiveComputation()); // 等价于 await expensiveComputation();
return 114514;
}
public static void main(String[] args) {
handle {
asyncFunc();
} with (YieldEffect(var computation)) {
new Thread(() -> {
var result = computation();
resume result;
}).run();
}
}
也就是说,async/await 在代数效应的语言中,不过是一个签名类似
effect YieldEffect<T>(computation: () -> T);
的一种代数效应而已,上面的伪代码和实际的 async/await 的唯一区别就在于我们的 resume result 没有考虑到异步上下文(恢复后的代码应该在哪个线程上执行)。
除开可以作为更多和控制流相关的语言特性的 building blocks 之外,代数效应自身也是类型系统的一部分,每个有副作用的函数,也就是拥有不被 handle-with 块所包裹的 perform 语句的函数,其签名中都会包含自身的副作用内容,我们可以将其签名中的 effectful 标记整合进函数自身的类型中,例如,上文中 bar 函数的类型就是 bar: void -> int effectful PrintEffect,同理,asyncFunc 函数的类型是 asyncFunc: void -> int effectful YieldEffect。如同 async 标记一样,副作用具有传递性,如果一个函数 baz 调用了包含副作用 A 的函数,且自身没有处理该副作用,那么 A 就同样会呈现在 baz 的签名中。
说了这么多有关代数效应的问题,我们需要思考下一个问题:java 的 checked exception 往往在文章中是被诟病的对象,而与其来自于同一种思想的代数效应却被你这么吹捧。这又是什么原因呢?要回答这个问题,我们就必须了解 checked exception 为什么被诟病。
首先,checked exception 并不支持在匿名函数,或者说 lambda 表达式上传播,这导致类似
strings.stream().forEach(Files::write)
的代码在 java 中几乎总是不合法的,因为 write 函数涉及 IO 操作,而 Files::write 又是一个匿名函数,无法承载 throws 标记,因此在类似的场景中我们都不得不写一串又臭又长的 try-catch 块:
strings.stream().forEach(text -> {
try {
Files.write(text);
} catch (IOException e) {
throw e;
}
})
而对于代数效应来说,由于我们将其作为类型系统中的一等公民,代数效应会自然而然地融入进一个匿名函数的类型中,对于匿名函数也不例外,在具有代数效应的语言中,Files.write 的签名无非是 Files.write: String -> void effectful IOEffect,而 forEach 对该函数不加处理的调用只是会将这个副作用向上传播而已,我们不需要在匿名函数中调用 Files.write 时强制加上对副作用的处理代码。
其次,java 的所有 throws 都需要开发者手动标记,如果调用链很长,甚至会出现一个函数的 throws 后面跟着十几个异常的情况,显得极其繁琐,这种问题在代数效应的世界中也不存在,由于代数效应被包含进了类型系统中,类型系统的推导算法可以轻松的计算出一个函数签名中应该包含哪些副作用,不包含哪些副作用,而完全不需要从程序员手动标注,这使得使用代数效应的代价被大大降低。
注(对于对类型理论有一定了解的人):代数效应的标记在类型可以被视为一种特殊的
record,我们可以在其上应用一种名为 row polymorphism 的算法来保证同一个函数可以接受拥有不同副作用标签的函数,在此之前,row polymorphism 大多用来保证代数数据类型之间的相容性,例如,一个接受{a: int, b: string}作为参数的函数,理应允许接受一个{a: int, b: string, c: char}类型的变量。同理,一个接受 sum typeTree<T> = Leaf(T) + Branch(Tree<T>, Tree<T>)作为参数的函数理应被允许接受一个DummyTree<T> = Leaf(T) + Branch(Tree<T>, Tree<T>) + Dummy类型的变量。这些例子的共同点是,如果一个函数接受A类型作为参数,那么一个包含A类型所有信息,同时还包含了一些“多余”信息的类型的变量同样应该被允许接受。同理,如果一个函数被要求接受含有PrintEffect副作用的函数作为参数;那么一个不仅具有PrintEffect,同时还具有YieldEffect副作用的函数也应该被允许。在没有子类型系统的编程语言中,这一过程是依赖 row polymorphism 实现的。
最后,checked exception 显得最为鸡肋的一点,是一旦异常被抛出,则整个上下文都会丢失,你不可能再回到异常被抛出的现场去继续执行,这导致 checked exception 对于异常这一副作用的记录毫无意义:异常被抛出时无论如何调用栈都会被 unwind 到最近的 try-catch 语句,追踪函数抛出了什么异常并不能带来任何优势。代数效应不仅避免了这一点,同时要注意,对于 checked exception 来说,异常是被实实在在抛出的,调用栈的 unwinding 也是确实发生的,异常处理机制确确实实是存在的,而对调用栈信息的收集是一个费时费力的过程,如果异常过多,这种行为及其影响运行效率。而对于代数效应而言,大部分代数效应的实现依赖于 one-shot delimited continuation,而 one-shot delimited continuation 的许多实现基于 CPS 变换这一纯粹语法层面的内容,也就是说,代数效应是一种编译器魔法,在运行时完全不存在,而代数效应中的“异常”副作用,同样不会留到运行时,在经过编译之后,代码中将不会留下任何代数效应的痕迹,因此,用代数效应去处理异常,其运行效率远高于一个实打实的 throw 语句。
注:对 one-shot delimited continuation 以及 CPS 变换的解释不在本文范围内,这两者每个都需要相当的篇幅来讲解,受长度所限不适合在此处提及,如果读者不知道这两者是什么,可以参考网上有关
async/await异步原理的大量相关文章,他们会详细的介绍什么是 CPS 变换,什么是 continuation。
由上面这几点可以看到,checked exception 之所以被人诟病,不是因为其核心思想存在问题,而是因为它的实现过于简陋,而代数效应系统几乎不存在 checked exception 的任何痛点,理应更受我们的青睐。在本文中,我们从 checked exception 出发,介绍了代数效应的工程价值,以及它是如何消除 java 中饱受诟病的 checked exception 的痛点的。在下一节中,我们将会从数学的角度来解释代数效应中“代数”的含义,以及代数效应的本质。










Comments NOTHING