如何使用精炼来表达约束大于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谓词支持Shapeless的类型级自然数()和整数单例类型(由Shapeless提供).所以以下约束做同样的事情:NatWitness

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

尽管如此,这仍然会使堆栈的大值变大,因此整数单例类型是你的情况.