scala - 如何使用精炼来表达常量 > 22 的约束

Question

我正在尝试通过改进(和无形)来探索改进类型检查的可能性。

我想用类型表示一些间隔或大小的约束。

所以，经过精炼，我可以写出这样的东西:

type Name = NonEmpty And MaxSize[_32]
type Driver = Greater[_15]

case class Employee(name : String @@ Name, age : Int @@ Driver = refineLit[Driver](18))

但是，我想用更大的自然来表达限制。

type BigNumber = Greater[_1000]

这个不行，因为 _1000没有定义。已经定义的最后一个是 _22我可以，无形Succ ，自己做的，不过很麻烦。

例子 :

type _25 = Succ[Succ[Succ[_22]]]
type _30 = Succ[Succ[Succ[Succ[Succ[_25]]]]]
type _40 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_30]]]]]]]]]]
type _50 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_40]]]]]]]]]]
type _60 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_50]]]]]]]]]]
type _70 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_60]]]]]]]]]]
type _80 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_70]]]]]]]]]]
type _90 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_80]]]]]]]]]]
type _100 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_90]]]]]]]]]]
// etc.

有没有更好的方法来表达这种约束，或者让 _1000以更有效的方式？
有什么我会错过的吗？

编辑:

我已经尝试过 Travis 命题:

val thousand = shapeless.nat(1000)

但这行导致 StackOverflowError在编译时(在宏扩展时)
如果我尝试使用较小的数字，则可以。

val limit = shapeless.nat(50)
type BigNumber = Greater[limit.N]

case class TestBigNumber(limit : Int @@ BigNumber)

在我的环境中，大于 400 的数字会引发 StackOverflowError。

此外，使用此代码，编译永远不会结束(使用 sbt):

val n_25 = shapeless.nat(25)
type _25 = n_25.N

val n_32 = shapeless.nat(32)
type _32 = n_32.N

val n_64 = shapeless.nat(64)
type _64 = n_64.N

Answer 1

Greater refined 中的谓词支持 Shapeless 的类型级自然数 ( Nat ) 和整数单例类型(由 Shapeless 的 Witness 提供)。所以以下约束做同样的事情:

import eu.timepit.refined.implicits._
import eu.timepit.refined.numeric._
import shapeless.{ Nat, Witness }
import shapeless.tag.@@

val a: Int @@ Greater[Nat._10] = 11
val b: Int @@ Greater[Witness.`10`.T] = 11

因为方式Nat和整数单例类型表示，后者不太可能使编译器溢出堆栈。例如，以下在我的机器上工作:

scala> val c: Int @@ Greater[Witness.`10000`.T] = 10001
c: shapeless.tag.@@[Int,eu.timepit.refined.numeric.Greater[Int(10000)]] = 10001

即使 10000远远超过了 shapeless.nat(10000)开始堆栈溢出。

作为脚注，可以使用 Nat表示大于 22 的值，而无需键入 Succ很多:

val hundred = shapeless.nat(100)
val c: Int @@ Greater[hundred.N] = 101

但是，对于大值，这仍然会破坏堆栈，因此在您的情况下，整数单例类型是可行的方法。