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

Question

这是我差不多两年前提出的一个问题的后续问题.我还在尝试使用类型系统来编写一个小的线性代数库,其中矢量/矩阵/张量的维度使用类型系统进行编码(使用Peano编号).这允许编译器将二进制操作限制为相应维度的对象.

它运行良好,但我必须手动指定每个维度类型.例如(使用无形自然数):

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

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

在Daniel Sobral回答评论时,我被告知这是不可能的,因为Scala不支持依赖类型.现在,Scala 2.10具有依赖类型和宏.有没有办法实现它？

Answer 1

现在可以使用2.10.0中的宏(尽管使用Paradise可以使语法更清晰).我已经发布了一个现成的,袖口完整的工作示例在这里 -我相信这很容易被更简洁,您可以使用像这样做:

val holder = NatExample.toNat(13)

然后:

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

如果传递非文字整数等,它将失败并出现合理的编译时错误.