自定义后端实践手册（Custom backend cookbook）

本文档介绍如何为 Idris 编译器实现自定义代码生成后端的详细方法。

本部分不涉及依赖类型相关实现细节。关于该部分，Edwin Brady 在 SPLV20 上有相关讲座，可在线获取。

Idris2 编译器的架构便于实现自定义代码生成后端。

扩展 Idris 以支持新后端的方法是将其作为库使用。模块 Idris.Driver 导出函数 mainWithCodegens，该函数接受 (String, Codegen) 列表，在启动时加载这些代码生成器（codegen），并以列表第一个为默认后端。

有意实现自定义后端的开发者需思考以下问题：

  • 自定义后端应采用哪种中间表示（IR，Intermediate Representation）？

  • 如何表示 Core.TT.Constant 类型定义的原始值？

  • 如何表示代数数据类型（Algebraic Data Types）？

  • 如何实现特殊值？

  • 如何实现原语操作（primitive operations）？

  • 如何编译 IR 表达式？

  • 如何编译定义（Definitions）？

  • 如何实现外部函数接口（Foreign Function Interface, FFI）？

  • 如何编译模块？

  • 如何嵌入代码片段？

  • 运行时系统应支持哪些内容？

首先，需要明确 Idris2 不是优化型编译器。目前其重点在于及时编译依赖类型函数式代码。其主要目标是验证程序在依赖类型环境下的正确性，并生成类似 λ 演算（lambda-calculus）的 IR，其中支持高阶函数。Idris 拥有三种用于代码生成的中间表示，每一层都更接近机器码，但需注意所有激进的代码优化应由自定义后端完成。生成代码的质量与可读性取决于后端实现者。Idris 默认编译为 scheme 时会在 IR 阶段擦除类型信息，无需保留类型。基于此，下面逐一解答上述问题。

Idris 后端的架构（The architecture of an Idris back-end）

Idris 会将其依赖类型前端语言编译为 Compile.TT.Term 表示。该数据类型有若干构造器，表示依赖类型项。此 Term 会被转换为 Core.CompileExpr.CExp，其构造器更多，结构类似带 let 绑定、结构化和带标签数据表示、原语操作、外部操作和 case 表达式的 λ 演算。CExp 更接近代码生成阶段。

自定义代码生成后端会获得定义上下文、模板目录和输出目录、待编译的 Core.TT.ClosedTerm 以及输出文件路径。

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String)
        -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term file = ?

ClosedTerm 是一种特殊的 Term，其未绑定变量列表为空。对于自定义后端的代码生成而言，这一技术细节并不重要，因为后端只需调用 getCompileData 函数生成 Compiler.Common.CompileData 记录。

CompileData 包含：

  • 一个主表达式（main expression），在 CExp 中作为程序入口。

  • Core.CompileExpr.NamedDef 列表

  • lambda-lifted 定义（Compiler.LambdaLift.LiftedDef）列表

  • Compiler.ANF.ANFDef 列表

  • Compiler.VMCode.VMDef 定义列表

这些列表包含：

  • 函数

  • 顶层数据定义

  • 运行时崩溃（如未填充的 hole、用户显式调用 idris_crash、case 树中的不可达分支）

  • 外部调用结构（Foreign call constructs）

自定义代码生成后端的任务是将某一阶段编码的定义（如 NamedDef、LiftedDef、CExp、ANF 或 VM）转换为代码生成器的中间表示。随后可进行优化并生成某种可执行形式。简言之，代码生成器需理解如何表示带标签数据和函数应用（即使是部分应用）、如何处理 let 表达式、如何实现和调用原语操作、如何处理 Erased 参数，以及如何处理运行时崩溃。

自定义后端实现者应选择最贴合目标技术抽象的 Idris IR，并考虑如何转换 CExp 形式的主表达式。Idris 本身不关注内存管理和线程，需由自定义后端为编译程序建模这些概念。一种做法是以较高级别语言为目标，尽量复用其能力；另一种是实现可处理内存管理和线程的运行时。

自定义后端应采用哪种中间表示（IR，Intermediate Representation）？

现在让我们关注 Idris 提供的不同中间表示（IR）。当使用 UsePhase 参数调用 getCompileData 函数时，它将生成一个 CompileData 记录，其中包含需要编译的顶层定义列表。这些定义包括：

  • NamedDef

  • LiftedDef

  • ANFDef

  • VMDef

这里需要回答的问题是：应该选择哪一个？哪一个最适合自定义后端？

如何表示 Core.TT.Constant 类型定义的原始值？

选择代码生成过程中使用的 IR 后，下一个需要回答的问题是如何在后端表示原语类型。Idris 有以下原语类型：

  • Int

  • ``Integer``（任意精度）

  • Bits(8/16/32/64)

  • Char

  • String

  • Double

  • ``WorldVal``（IO 计算的令牌）

由于 Idris 允许对类型进行模式匹配，所有原语类型都有对应的类型描述原语：

  • IntType

  • IntegerType

  • Bits(8/16/32/64)Type

  • StringType

  • CharType

  • DoubleType

  • WorldType

这些原语类型的表示方式需要经过深思熟虑的设计决策，因为它会影响代码生成的许多部分，例如涉及 FFI 时后端值的转换、运行时大部分数据都以这些形式表示。原语类型的表示会影响可能的优化技术，也会影响内存管理和垃圾回收。

有两个特殊的原语类型：String 和 World。

String

顾名思义，这种类型表示字符序列。如`原语 FFI 类型 <https://idris2.readthedocs.io/en/latest/ffi/ffi.html#primitive-ffi-types>`_中所述，字符串以 UTF-8 编码。

对于非 Idris 运行时创建的 String，由谁负责释放内存并不总是明确的。Idris 中创建的字符串总是有值的，这与宿主技术可能的字符串表示不同，后者可能允许 NULL 指针作为值，这在 Idris 中是不可能的。这限制了自定义后端中字符串的可能表示方式，偏离 Idris 的表示方式并不是个好主意。最佳方案是在自定义后端的字符串表示和运行时之间构建一个转换层。

World

在纯函数式编程中，当需要维护子表达式执行顺序时，必须表示因果关系。在 Idris 中，使用一个标记（token）来链接 IO 函数调用。这是关于世界状态的抽象概念。例如，这些信息可能是运行时需要用于记录运行程序状态的信息。

Idris 程序中的 WorldVal 值通过 primIO 构造访问，这会引导我们到 PrimIO 模块。让我们看看相关的代码片段：

data IORes : Type -> Type where
     MkIORes : (result : a) -> (1 x : %World) -> IORes a

fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
fromPrim op = MkIO op

primIO : HasIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
primIO op = liftIO (fromPrim op)

在 Idris 中，世界值以 %World 引用。它由运行时在程序启动时创建。其内容由自定义运行时更改。更准确地说，World 是在程序执行过程中对 WorldVal 求值时创建的。这可能发生在程序初始化时或执行 unsafePerformIO 函数时。

如何表示代数数据类型（Algebraic Data Types）？

在 Idris 中定义数据类型有两种不同方式：使用 data 关键字引入标记联合（tagged unions），使用 record 关键字声明结构体。声明 record 相当于定义一个命名字段集合。让我们看看这两种方式的例子：

data Either a b
  = Left  a
  | Right b

record Pair a b
  constructor MkPair
  fst : a
  snd : b

Idris 不仅提供代数数据类型，还提供索引族（indexed families）。这些是标记联合，其中不同的构造器可能有不同的返回类型。这里以 Vect 为例，它是一个索引族数据类型，对应一个在编译时已知长度的链表。它有一个索引（类型为 Nat）表示列表长度（因此 [] 和 (::) 构造器的这个索引值不同）和一个参数（类型为 Type）对应列表中存储的值的类型。

data Vect : (size : Nat) -> Type -> Type where
  Nil  : Vect 0 a                         -- empty list: size is 0
  (::) : a -> Vect n a -> Vect (1 + n) a  -- extending a list of size n: size is 1+n

data 和 record 都被编译为中间表示中的构造器。这类构造器的两个例子是 Core.CompileExpr.CExp.CCon 和 Core.CompileExpr.CDef.MkCon。

编译 Either 数据类型将在 IR 中生成三个构造器定义：

  • 一个用于 Either 类型本身，参数个数为 2。参数个数（arity）表示构造器应有多少参数。此处为 2，符合 Idris 原始 Either 类型有两个参数的设定。

  • 一个用于 Left 构造器，参数个数为 3。虽然在 Idris 中该构造器只有一个参数，但还需考虑数据类型的类型参数。

  • 一个用于 Right 构造器，参数个数为 3。

在 IR 中，构造器具有唯一名称。为提高效率，Idris 会为每个数据构造器分配唯一的整数标签（tag），这样构造器匹配只需比较整数而非字符串。在上述 Either 示例中，Left 的标签为 0，Right 的标签为 1。

构造器可视为结构化信息：由名称和参数组成。自定义后端需决定如何表示此类数据。例如在 Python 中可用 Dict，在 JavaScript 中可用 JSON。最重要的是，这些结构化值属于堆相关值，应动态创建和存储。如果宿主技术易于映射，可直接复用其内存管理，否则需自行实现合适的内存管理。例如 RefC C 后端就基于引用计数实现了自己的内存管理。

如何实现特殊值？

除了数据构造器外，Idris IR 还存在两类特殊值：类型构造器和 Erased。

类型构造器（Type constructors）

与程序运行时行为无关的类型和数据构造器可在编译期使用，但会从中间表示中被擦除。

但有些类型构造器即使在运行时也需保留，因为 Idris 允许对类型进行模式匹配：

notId : {a : Type} -> a -> a
notId {a=Int} x = x + 1
notId x = x

在此我们可以对 a 进行模式匹配，确保 notId 在 Int 类型和其他类型上表现不同。这会生成包含 Case 表达式的 IR，其中有两个分支：一个 Alt 匹配 Int 类型构造器，另一个为 notId 函数的非 Int 匹配默认分支。

这其实并不特殊：Type 有点像一个包含所有用户可能声明或使用类型的无限数据类型。后端和宿主语言可用处理数据构造器的同样机制来处理它。原因在于依赖类型语言中，类型层和值层表达式都用同一种语言构造，类型层项的编译方式与值层项一致。这正是依赖类型抽象优雅之处。

``Erased``（已擦除）

另一类特殊值是 Erased。如果原始值仅在类型推导过程中需要，Idris 编译器会在 IR 中生成 Erased。例如：

data Subset : (type : Type)
           -> (pred : type -> Type)
           -> Type
  where
    Element : (value : type)
           -> (0 prf : pred value)
           -> Subset type pred

由于 prf 的数量为 0，编译时必然被擦除，运行时不会出现。因此，prf 在 IR 中会被表示为 Erased。自定义后端也需像处理其他数据值一样处理该值，因为它可能出现在普通值的位置。最简单的做法是将其实现为特殊数据构造器，交由宿主技术的优化机制移除。

如何实现原语操作（primitive operations）？

原语操作定义在模块 Core.TT.PrimFn 中。该数据类型的构造器表示自定义后端需实现的原语操作。这些操作可分为：

  • 算术操作（Add、Sub、Mul、Div、Mod、Neg）

  • 位操作（ShiftL、ShiftR、BAnd、BOr、BXor）

  • 比较操作（LT、LTE、EQ、GTE、GT）

  • 字符串操作（Length、Head、Tail、Index、Cons、Append、Reverse、Substr）

  • 双精度浮点操作（Exp、Log、Sin、Cos、Tan、ASin、ACos、ATan、Sqrt、Floor、Ceiling）

  • 数值和字符串的类型转换（Casting）

  • 不安全的类型转换操作 BelieveMe

  • Crash 操作用于接收类型和字符串，通过抛出错误在该类型下创建一个值。

BelieveMe（不安全类型转换）

原语 believe_me 是一种不安全的类型转换，允许用户在确信某事为真但无法证明时绕过类型检查器。

例如，假设 Idris 的原语实现正确，如果对两个 Int``（``i 和 j）的布尔等值测试返回 True，则 i 和 j 应相等。此时可用 believe_me 将 Refl``（命题等价证明的构造器）从 ``i === i 强制转换为 i === j。在这种情况下，实现是安全的。

装箱（Boxing）

Idris 假定后端的数据表示不是强类型的，所有数据类型采用相同的表示方式。这会对原语和构造器数据类型的表示带来约束。一种解决方案是自定义后端将原语数据类型与构造器一样用特殊标签表示，这称为装箱（boxing）。

官方后端将原语数据类型以装箱形式表示。

  • RefC：对原语类型进行装箱，便于放入堆中。

  • Scheme：将 Constant 类型的值以 Scheme 字面量输出。

如何编译顶层定义？

如前所述，Idris 在 CompileData 记录中提供了 4 种不同的 IR：Named、LambdaLifted、ANF 和 VMDef。组装 CompileData 时需告知 Idris 编译器关注哪个层级。CompileData 包含的定义列表可视为自定义后端需生成函数的顶层定义。

代码生成后端需支持四类顶层定义：

  • 函数（Function）

  • 构造器（Constructor）

  • 外部调用（Foreign call）

  • 错误（Error）

函数 包含类似 λ 演算的表达式。

构造器 表示数据或类型构造器，应实现为在自定义后端中创建相应数据结构的函数。

顶层 外部调用 定义了调用 Idris 程序外部实现函数的入口。Foreign 结构包含程序员定义的代码片段字符串列表、参数类型和外部函数返回类型。自定义后端应生成包装函数，详见“如何实现外部函数接口（Foreign Function Interface）？”一节。

顶层 错误 定义表示 Idris 程序中的 hole、对 idris_crash 的调用或 case 树中的不可达分支。用户可为测试目的执行不完整程序，只要实际不会用到任何 hole 的值即可。库作者可在遇到不可恢复错误时抛出异常。最后，Idris 会将 case 树的不可达分支编译为运行时错误，因为这些本就是死代码。

如何编译 IR 表达式？

自定义后端应决定以哪种中间表示为起点。转换结果应为宿主技术的表达式和函数。

ANF 和 Lifted 中的定义以树状表达式表示，控制流基于 Let 和 Case 表达式。

Case 表达式（Case expressions）

Case 表达式有两种类型：一种用于匹配和分支原语值（如 Int），另一种用于匹配和分支构造器值。这两种 case 表达式的分支备选项分别用 ``ConstCase``（匹配常量值）和 ``ConCase``（匹配构造器）表示。

对构造器的匹配可通过标签（tag）匹配实现，也可用构造器名称匹配（效率较低）。无论哪种方式，匹配时都应将构造器参数的值绑定到分支体中的变量。具体实现方式取决于宿主技术，如 switch 表达式、带模式匹配的 case、if-then-else 链等。

模式匹配绑定变量时，参数个数可能与顶层定义和 GlobalDef 中构造器的参数个数不同。这是因为类型检查阶段会保留所有参数，但 case 树的代码生成器会移除被标记为 erased 的参数。自定义后端的代码生成器也需在构造器实现中移除这些参数。GlobalDef 的 eraseArg 字段包含此信息，可用于确定需保留的参数数量。

值的创建（Creating values）

值的创建有两种方式。

若为原语值，会以 PrimVal 形式传递给后端，应根据“如何表示原语值”一节的设计决策编译为宿主语言常量。

若为结构化值（如 Con），应编译为宿主语言中创建动态值的函数。“如何表示构造器值”一节的设计决策将在此生效。

函数调用（Function calls）

函数调用分为四类：- 饱和调用（参数齐全）- 不足调用（缺少部分参数）- 原语函数调用（必为饱和，PrimFn 构造器）- 外部函数调用（通过名称引用）

ANF 和 Lifted 中间表示都支持函数的部分应用（通过各自的 UnderApp 构造器）。自定义后端需要支持函数的部分应用以及在宿主技术中创建闭包。对于 Scheme 这样的后端来说这不是问题，因为它们天然支持函数的部分应用。但如果宿主语言没有这个功能，自定义后端就需要模拟闭包。一种可能的解决方案是将闭包实现为一个特殊对象，用于存储函数及其当前已应用的参数值，直到收到所有必要参数后再进行求值。如果选择 VMCode 中间表示进行代码生成，也需要采用相同的方法。

Let 绑定（Let bindings）

ANF 和 Lifted IR 都有 Let 构造，可为局部变量赋值。两者在绑定变量的表示上有所不同。

Lifted 是以作用域内局部变量 List Name 为索引的类型族。变量用 LLocal 构造器表示，存储一个 Nat 及其指向有效局部变量名的证明。

ANF 是更低层次的表示，不再具备上述保证。局部变量用 AV 构造器表示，存储一个 AVar``（定义见下文）。``ALocal 构造器存储一个 Int，对应于 Lifted 中的 Nat。ANull 构造器表示已擦除变量，其在宿主语言中的表示取决于“如何表示 Erased 值”一节的设计。

VMDef 特性（VMDef specificities）

VMDef 旨在作为最接近机器码的 IR。在 VMDef 中，所有定义都被编译为小型虚拟机的寄存器和闭包指令。

在该层级，不再有 Let 表达式，只有 ASSIGN 语句。

此层级不再通过 Case 表达式绑定变量，而是 CASE 根据构造器本身选择分支。引入了 PROJECT 操作用于按位置显式提取构造器参数。

不再有 App 或 UnderApp，均由 APPLY 替代，后者每次只应用一个值并创建闭包。对于已擦除值，NULL 操作用于为寄存器赋空值。

如何实现外部函数接口（Foreign Function Interface, FFI）？

外部函数接口（FFI）在 Idris 程序运行中起着重要作用。上述原语操作主要用于值操作，并不涉及与运行时系统的复杂交互。许多原语类型可视为通过 external 和外部函数提供的抽象类型，用于操作这些值。

自定义后端和宿主技术的责任是以操作上正确的方式表示这些计算。宿主技术中原语类型的表示设计必然影响 FFI 的设计。

外部类型（Foreign Types）

Idris 最初有官方 C 后端实现，尽管后来发生变化，FFI 类型名称仍保留 C 前缀。Core.CompileExpr.CFType 包含如下定义，多数与原语类型一一对应，部分需额外说明。

外部类型包括：

  • CFUnit

  • CFInt

  • CFUnsigned(8/16/32/64)

  • CFString

  • CFDouble

  • CFChar

  • CFFun 类型为 CFType -> CFType -> CFType。宿主技术可通过 CFFun 类型参数注册回调。后端应能处理 Idris 端定义并编译到宿主技术的函数。若自定义后端支持高阶函数，应据此实现对该类 FFI 类型的支持。

  • CFIORes 类型为 CFType -> CFType。所有 PrimIO 定义的计算都会有此额外层。纯函数在宿主技术实现的运行时中不应对程序状态产生可观察的 IO 效果。注意：注册回调函数时也会用到 IORes。

  • CFWorld 表示当前世界状态，应指代函数调用间传递的令牌。World 值的实现应包含后端特定值及 Idris 运行时状态信息。

  • CFStruct 类型为 String -> List (String, CFType) -> CFType，对应 System.FFI.Struct 的外部类型。在自定义后端中表示类似 C 的结构体。应实现 prim__getField 和 prim__setField 原语以支持该类型。

  • CFUser 类型为 Name -> List CFType -> CFType。用 [external] 定义的类型用 CFUser 表示。例如 data MyType : Type where [external] 会被表示为 CFUser Module.MyType []。

  • CFBuffer 是为 Data.Buffer 定义的外部类型。尽管属于外部类型，Idris 以随机访问缓冲区为基础。

  • CFPtr：Ptr t 和 AnyPtr 会被编译为 CFPtr。无法用简单原语表示的复杂结构化数据可用此类型追踪值的使用位置。在 Idris 中，Ptr t 定义为外部类型。

  • CFGCPtr：GCPtr t 和 GCAnyPtr 会被编译为 CFGCPtr。GCPtr 由调用 onCollect 的 Ptr 值推断而来，具备特殊属性。onCollect 为指针附加终结器，在指针释放时运行。

示例（Examples）

让我们回到 Idris 源码层面，看看如何表示这些内容。涉及 FFI 的最简单定义形式是带有 %foreign 编译指示的函数定义。该指示接受字符串列表，表示后端到外部调用名称的映射。例如：

该函数应由 C 后端翻译为对 smallc.c 文件中 add 函数的调用。在 FFI 中，Int 被翻译为 CFInt。后端假定库文件中指定的数据表示与普通 Idris 值一致。

我们还可以如下定义 external 类型：

此处 ThreadID 被定义为外部类型，内部表示为 CFUser "ThreadID" []。由 scheme 运行时创建的值视为黑盒。

prim__fork 翻译为外部类型后，其类型为 [%World -> IORes Unit, %World] -> IORes Main.ThreadID。可见 %World 被添加到 IO 计算中，且始终为参数列表最后一项。

对于 FFI 函数，其类型信息和用户自定义字符串可在顶层定义中找到。自定义后端应利用这些定义生成包装代码，将 CFType 描述的类型转换为 %foreign 指令所需类型。

如何编译模块？

Idris 编译器为模块生成中间文件，这些文件的内容既不属于 Lifted、ANF，也不属于 VMCode。因此，当编译流水线进入代码生成阶段时，所有信息都将位于 CompileData 记录的一个实例中，自定义代码生成器后端可以像看到整个程序一样处理它们。

自定义后端可以选择为不同命名空间中的函数引入一些层次结构，并组织一些模块结构，让主机技术以不同大小的块处理各个部分。然而，此功能不在 Idris 编译器的范围内。

值得注意的是，Idris 中的模块可以是相互递归的。因此，将 Idris 模块直接编译为主机语言的模块可能会失败。

如何嵌入代码片段？

为 Idris 实现自定义后端的一个可能动机是生成用于更大项目的代码。该项目可能绑定到另一种具有许多有用库的语言，但可以在某些地方受益于 Idris 强大的类型系统。

为此编写代码生成器时，基于外部接口的主机技术和 Idris 之间的互操作性可能不太方便。在这种情况下，自然需要嵌入主机技术的代码。精化（Elaboration）可以解决这个问题。

精化是一种类型检查时的代码生成技术。它依赖 Elab 单子来编写脚本，这些脚本可以与类型检查机制交互，在 Core.TT 中生成 Idris 代码。

当需要嵌入代码片段时，应随自定义后端提供自定义库，将有效的代码片段转换为它们在 Core.TT 中的表示。

运行时系统应支持哪些内容？

总之，Idris 编译器的自定义后端应在主机技术中创建一个能够运行 Idris 程序的环境。由于 Idris 是函数式编程语言家族的一部分，其计算模型基于图归约。在内存中表示为简单图的程序基于求值期间的闭包创建机制。闭包创建甚至存在于最低级别的 IR 中。因此，任何主机技术中的运行时都需要支持某种闭包表示，并能够将它们存储在堆上，因此内存管理的责任落在自定义后端实现者的肩上。如果主机技术有内存管理，这个问题并不困难。通过主机技术的工具也很容易实现闭包存储。

虽然尚不清楚后端应支持多少功能。Scheme 后端的工具通过外部类型和围绕它们的原始操作被引入 Idris 世界。这是一个很好的实践，让社区能够专注于实现依赖类型语言的快速编译器。这些隐藏功能之一是并发原语。这些是不同库的一部分，可能是编译器的一部分，也可能是贡献包的一部分。如果主机技术的线程模型与 Idris 默认后端当前从 Scheme 技术继承的不同，这可能是一项更大的工作。

Idris 中的 IO 使用抽象的 %World 值实现，该值作为通过简单调用底层运行时系统与世界交互的函数的令牌。程序的入口点是 main 函数，它具有 IO 单元类型，如 main : IO ()。这意味着每个运行的程序都从其 IO 计算的一部分开始。在底层，这是通过创建 %World 抽象值并调用 main 函数实现的，该函数被编译为传递抽象 %World 值用于 IO 相关的外部或外部操作。

PrimIO 模块中有一个名为 unsafePerformIO 的操作。unsafePerformIO 的类型签名表明它能够在纯上下文中求值 IO 计算。在底层，它的运行方式与 main 函数完全相同。它生成一个新的 %World 令牌并将其传递给 IO 计算。这引出了一个设计决策：如何表示 World 的状态，以及如何表示通过 unsafeCreateWorld 为 unsafePerformIO 操作实例化的世界？main 和 unsafeCreateWorld 的机制都使用 %MkWorld 构造器，该构造器将被编译为 WorldVal，其类型为 WorldType，这意味着运行时的实现负责创建围绕 World 的抽象。抽象 World 值的实现可以基于单例模式，即只有一个世界，或者可以有多个世界，从而为 unsafePerformIO 创建平行宇宙。