Tagless Final

发布于 2022/02/06 - 修改于 2022/08/15 - 大约需要 3 分钟 - 1292 字

所谓Tagged

在设计嵌入式领域特定编程语言的时候，首先会有语法。很多语言都是通过代数数据类型来定义。我们以一个允许布尔值和整数值并且定义了比较的例子看下。表达式可以为布尔值、整数、比较，那自然的会有如下定义：

enum Exp {
    case EBool(v: Boolean)
    case EInt(v: Int)
    case EEq(v1: Exp, v2: Exp)
}

可以看出这种代数数据类型是带标签的，也就是EBool或EInt或EEq。

这会有一个问题：对于带类型的嵌入式领域特定语言，我们无法直接借助元语言/宿主语言（在这个例子中是Scala）来辅助进行类型检查。我们可以写出例如EEq(EBool(true), EInt(1))的表达式，它能通过元语言的类型检查，只有在解析后才能抛出错误。

所谓Tagless

广义代数数据类型（GADT），允许我们在代数数据类型之上添加一个类型参数。按照上面的例子，我们会有如下GADT定义：

enum Exp[T] {
    case EBool(v:Boolean) extends Exp[Boolean]
    case EInt(v: Int) extends Exp[Int]
    case EEq(v1: Exp[T], v2: Exp[T]) extends Exp[Boolean]
}

可以看到我们无法再写出类似EEq(EBool(true), EInt(1))的表达式了：Scala的类型检查足以发现它的错误。

在这种情况下，EBool可以被视作一个Boolean => Exp[Boolean]的函数，这也许是其被称为Tagless的原因。

所谓Tagless Final

之前的定义被称作"Initial"，因此为了与之区别开，这种新的定义方式便被称为Final。

import cats.Eq
trait Exp[F[_]] {
    def eBool(v1: Boolean): F[Boolean]
    def eInt(v: Int): F[Int]
    def eEq[T](v1: F[T], v2: F[T])(using Eq[T]): F[Boolean]
}

可以看出这样的定义只是一组函数的定义而已，或者说一个接口，并不存在代数类型，自然也没有所谓的标签了。

运算

对于Initial的表达式，如果我们需要运算或者序列化，我们只需要模式匹配即可，例如：

import Exp._
def eval(e: Exp[T]): T = e match {
    case EInt(v) => v
    case EBool(v) => v
    case EEq(v1, v2) => eval(v1) == eval(v2)
}

def serialize(e: Exp[T]): String = e match {
    case EInt(v) => s"${v}"
    case EBool(v) => s"${v}"
    case EEq(v1, v2) => s"${v1} == ${v2}"
}

而对于Final的表达式，我们只需要提供一个接口的实现，例如：

import cats.Id
given eval: Exp[Id] with {
    def eBool(v: Boolean) = v
    def eInt(v: Int) = v
    def eEq[T](v1: Id[T], v2: Id[T])(using eq: Eq[T]) = eq.eqv(v1, v2)
}

import cats.data.Const
type Str[T] = Const[String, T]
given serialize: Exp[Str] with {
    def eInt(v: Int) = Const(s"${v}")
    def eBool(v: Boolean) = Const(s"${v}")
    def eEq[T](v1: Str[T], v2: Str[T])(using Eq[T]) = Const(s"${v1.getConst} == ${v2.getConst}")
}

调用

对于Initial的实现方式，我们有：

import Exp._
val exp = EEq(EInt(5), EInt(6))
eval(exp)
serialize(exp)

而对于Final，我们有：

import eval._
eEq(eInt(5), eInt(6))

和

import serialize._
eEq(eInt(5), eInt(6)).getConst

可以看出两种实现的表达形式非常相近，两者之间有着密切的联系。

优点

Tagless Final有不少的优点。这里仅列出一项。

组合性

Final的实现可以带来组合性。设想下我们要在之前的基础上加上整数的加法。

对于Initial的实现，我们首先要更改数据结构的声明：

enum Exp[T] {
    case EBool(v:Boolean) extends Exp[Boolean]
    case EInt(v: Int) extends Exp[Int]
    case EEq(v1: Exp[T], v2: Exp[T]) extends Exp[Boolean]
    case EAdd(v1: Exp[Int], v2: Exp[Int]) extends Exp[Int] // 额外添加
}

之后我们要修改先前所有的函数中的类型匹配，否则类型匹配不完全。

而对于Final的实现，我们只需要另外再额外声明一个接口：

trait ExpExt[F[_]] {
    def eAdd[T](v1: F[T], v2: F[T])(using Integral[T]): F[T]
}

之后只需要再提供这个接口的实现就可以了，丝毫不影响原有的实现：

given ext: ExpExt[Id] with {
    def eAdd[T](v1: Id[T], v2: Id[T])(using i: Integral[T]) = i.plus(v1, v2)
}
import eval._
import ext._
eEq(eInt(5), eAdd(eInt(2), eInt(3))) // 返回true

总结

这里只是管中窥豹，略微介绍。有兴趣的朋友可以参阅参考资料，相信一定会大有裨益。

（或者待我日后再来补充，发出鸽子的声音.jpg）

参考资料

O. Kiselyov, “Typed Tagless Final Interpreters,” in Generic and Indexed Programming, vol. 7470, J. Gibbons, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 130–174. doi: 10.1007/978-3-642-32202-0_3.

以上资料可以在Oleg教授的网站上看。

编程语言