如何使用 refined 来表达常数大于 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)

但是这一行在编译时（在宏扩展时）导致 WhosebugError 如果我尝试使用较小的数字，就可以了。

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

case class TestBigNumber(limit : Int @@ BigNumber)

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

此外，使用这段代码，编译永远不会结束（使用 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

refined 中的 Greater 谓词同时支持 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

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

如何使用 refined 来表达常数大于 22 的约束

How using refined to express constraints with constants > 22

scala

shapeless