上一篇文章介绍了 shapeless 的重要功能:自动派生 typeclass 实例。
本文将阐述一个看起来没什么作用,但实际上是 shapeless 关于泛型编程的重要基石: Nat (自然数)

皮亚诺公理(Peano axioms)

首先我们确定一下自然数只是一个符号系统,我们用 0,1,2,… 这些符号表示一些抽象的概念

皮亚诺公理告诉我们这个符号系统有三个组成元素

  • 一个初始元素(比如0) x
  • 一个集合 X
  • 一个 X 到自身的映射(后继关系) f

并且这个系统满足以下公理

  1. x 属于 X (0是自然数)
  2. x 不在 f 的值域内 (0 不是任何数的后继)
  3. 如果 f(a) = f(b)a = b (即 f 是一个单射)
  4. 若 a 属于 X,则 f(a) 属于 X
  5. 若 A 为 X 子集,并满足
    • x 属于 A, 且
    • 若 a 属于 A,则 f(a) 属于 A
      则 A = X

基于上述公理就可以建立一阶算术系统

Nat 类型与自然数对应关系

1
2
3
4
5
6
7
8
9
10
11
trait Nat {
type N <: Nat
}
case class Succ[P <: Nat]() extends Nat {
type N = Succ[P]
}
class _0 extends Nat with Serializable {
type N = _0
}

很容易就可以总结出 Nat 类型和自然数的对应关系

  • X 为 所有 Nat 子类型
  • Succ(后继)为映射 f,注意一个类型构造器可以看作是一个映射
  • _0 为初始元素

Nat 与上述公理对应关系

  • 第 1 条,_0 是 Nat 子类型
  • 第 2 条,_0 显然不是任何类型的 Succ,scala 编译器的类型检查可以保证 Succ[P] 不等于 _0
  • 第 3 条,假设存在 A, B 满足 A != B 且 Succ[A] = Succ[B],同样编译器类型检查可以保证如果 A != B,则 Succ[A] != Succ[B],即 Succ 是一个单射
  • 第 4 条,Succ 的定义直接指出如果 P 是 Nat,则 Succ 亦是 Nat
  • 第 5 条,A 就是 Nat 类型的定义,(这里形式化证明过于困难,暂不做证明)

加法定义

有了上述公理之后,可以建皮亚诺算术系统,我们以加法为例
加法定义为满足以下关系的映射

  1. a + 0 = a
  2. a + Succ(b) = Succ(a + b)

在 shapeless 里,加法定义如下(Aux 类型的作用参考此处)

1
2
3
4
5
6
7
8
9
10
11
trait Sum[A <: Nat, B <: Nat] extends Serializable { type Out <: Nat }
object Sum {
type Aux[A <: Nat, B <: Nat, C <: Nat] = Sum[A, B] { type Out = C }
// 对应 1 处定义
implicit def sum1[B <: Nat]: Aux[_0, B, B] = new Sum[_0, B] { type Out = B }
// 此处定义与 2 处略有不同
implicit def sum2[A <: Nat, B <: Nat, C <: Nat]
(implicit sum : Sum.Aux[A, Succ[B], C]): Aux[Succ[A], B, C] =
new Sum[Succ[A], B] { type Out = C }
}

这里第 2 条规则定义为 Sum[A, Succ[B]].C = Sum[Succ[A] , B].C,而加法的第二个规则则要求 Sum[A, Succ[B]].C = Succ[Sum[A, B].C]
shapeless 这里定义实际上可以推导出第 2 规则。

将上述类型转换成命题: a + S(b) = S(a) + b => a + S(b) = S(a + b)

下面是证明过程 (S 为后继映射,即 Succ)

  • b = 0 时 a + S(0) = S(a) + 0 = S(a) = S(a + 0)
  • 假设 b = x 时, a + S(x) = S(a + x) 成立,则 b = S(x) 时 a + S(S(x)) = S(a) + S(x) = S(S(a) + x) = S(a + S(x)),可以得出对于 b = S(x) ,a + S(b) = S(a + b) 也成立
  • 上述两者归纳得出命题成立

现在来看看如何使用 Sum 来约束类型

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
object alias {
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
}
import alias._
def check[A <: Nat, B <: Nat](implicit sum: Sum.Aux[A, B, _3]) = {}
check[_0, _3]
check[_1, _2]
check[_2, _1]
check[_3, _0]
check[_1, _1] // 编译错误

上述 check 方法要求两个类型的 Sum_3,可以看只有 Sum_3AB 类型才能通过编译

总结

本文介绍了 shapeless 的重要基础类型 Nat,理解该类型是掌握 shapeless 其他类型的重要前提