scala - 使用类型系统将整数转换为 Peano 数

Question

这是a question I asked almost two years ago的后续.我仍在尝试使用类型系统来编写一个小型线性代数库，其中向量/矩阵/张量的维度使用类型系统(使用 Peano 编号)进行编码。这允许编译器将二进制操作限制为对应维度的对象。

它运行良好，但我必须手动指定每个维度类型。例如(使用 shapeless natural numbers ):

type _1 = Succ[Nat._0]
type _2 = Succ[_1]
type _3 = Succ[_2]

小尺寸没问题，但如果我需要定义尺寸 _1024 会很无聊.我正在尝试(但没有成功)找到一种方法(在编译时)将整数文字转换为相应的 Peano-number 类型。

在 Daniel Sobral answer评论，有人告诉我这是不可能的，因为 Scala 不支持依赖类型。现在，Scala 2.10 既有依赖类型又有宏。那么有没有办法实现它？

Answer 1

现在使用 2.10.0 中的宏就可以做到这一点(尽管 Paradise 的语法会变得更清晰)。我已经发布了一个即兴的完整工​​作示例 here ——我相信它可以很容易地变得更简洁——你可以这样使用:

val holder = NatExample.toNat(13)

进而:

scala> implicitly[holder.N =:= shapeless.Nat._13]
res0: =:=[holder.N,shapeless.Nat._13] = <function1>

如果您传递非文字整数等，它将因合理的编译时错误而失败。