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

发布时间：2020-12-16 18:52:58 所属栏目：安全来源：网络整理

导读：这是 a question I asked almost two years ago的后续跟踪.我仍在尝试使用类型系统来编写一个小的线性代数库,其中矢量/矩阵/张量的维度使用类型系统进行编码(使用Peano编号).这允许编译器将二进制操作限制为相应维度的对象. 它运行良好,但我必须手动指定每个

这是 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具有依赖类型和宏.有没有办法实现它？

解决方法

现在可以使用2.10.0中的宏(尽管使用Paradise可以使语法更清晰).我已经发布了一个完整的工作示例 here – 我确信它可以轻松地变得更加简洁 – 您可以像这样使用：

val holder = NatExample.toNat(13)

然后：

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

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

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!