core 设计

本页解释为什么要有 core 门面包,以及为什么它恰好包含 Dual[T] 环层面的词汇。

设计目标

为只需要对偶数代数的代码提供最小的导入:环运算、单位元和整数常量,不包含 arithmetic 的解析 trait 和错误类型。

数学背景

许多可微程序都是多项式形式的:它们只用到 ++、−-、×\times 和整数常量。对于这类程序,dual 设计 中的恒等式

p(a+bε)=p(a)+p′(a) b εp(a + b\varepsilon) = p(a) + p'(a)\,b\,\varepsilon

在任何交换环中都成立,因此这类代码所需要的就是 trait Zero、One、AddMonoid、AddGroup、MulMonoid、Semiring、Ring 以及典范映射 Z→T\mathbb Z \to T(IntegralHomomorphism)。门面包恰好重新导出这些 trait,对应于如下层次

AddMonoid⊂AddGroup,AddMonoid+MulMonoid⊂Semiring⊂Ring\texttt{AddMonoid} \subset \texttt{AddGroup},\quad \texttt{AddMonoid} + \texttt{MulMonoid} \subset \texttt{Semiring} \subset \texttt{Ring}

它们在 T[ε]T[\varepsilon] 上的实例推导见 dual 设计。

设计决策

为代数部分单独设立门面包

问题。 根包还重新导出了解析 trait 和带检查的错误类型,它们属于生态中的另一层。

选择。 core 只重新导出 Dual 和 luna-generic 的结构 trait。它的 moon.pkg 只导入 dual 和 luna-generic,因此阅读导入列表的人就能看出代码是纯代数的。

重新导出,而非重新定义

与 autodiff 设计 一样,这些名称都是原始 trait 的 pub using 别名,因此实例与 Luna Flow 的其余部分共享。

正确性与不变量

  • core 不定义任何条目;它的接口文件只包含 pub using 语句。
  • 它依赖 autodiff/dual 和 luna-generic,除此之外不依赖任何东西。
  • 每个重新导出的 trait 在 T 满足相应约束时都在 Dual[T] 上有实例。

被否决的方案

  • 把 core 并入根包。 根包还携带了 arithmetic;把代数部分分开能让这种分层清晰可见。
  • 重新导出 Field 或 Inverse。 Dual[T] 并未实现它们,因此它们只会诱使用户写出无法满足的约束。

边界

  • 没有解析 trait,没有带检查的运算,也没有驱动函数。
  • 没有 Field、MulGroup、Inverse 或 NatHomomorphism。