使用类型系统将整数转换为 peano 数答案

【问题标题】：Converting integers to peano numbers using the type system使用类型系统将整数转换为 peano 数
【发布时间】：2012-12-21 00:15:12
【问题描述】：

这是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 数字类型的方法。

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

【问题讨论】：

由于 2.10 只支持 def 宏，我想你应该看看宏天堂里的类型宏：docs.scala-lang.org/overviews/macros/paradise.html
Scala 支持依赖类型？我能介绍一下这方面的背景吗？
@Bill 看看宏示例。宏结果类型是依赖类型。
呵呵，我从来没有这么想过。这很酷。谢谢，@paradigmatic。

【解决方案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>

如果您传递一个非文字整数等，它将失败并出现合理的编译时错误。

【讨论】：

在这种情况下 =:= 运算符是什么意思？
standard library type class 提供了编译器知道两种类型相同的证据。它大约在 2.10 之前——例如，请参阅 this answer，了解它的使用方式。