scala – 如何使用精炼来表达约束的常量> 22
发布时间：2020-12-16 08:58:19 所属栏目：安全 来源：网络整理
导读：我试图通过改进(和无形)来探索改进类型检查的可能性. 我想用类型来表示间隔或大小的一些约束. 所以,通过精炼,我可以写出这样的东西： type Name = NonEmpty And MaxSize[_32]type Driver = Greater[_15]case class Employee(name : String @@ Name,age : Int
|
我试图通过改进(和无形)来探索改进类型检查的可能性.
我想用类型来表示间隔或大小的一些约束. 所以,通过精炼,我可以写出这样的东西： 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 示例： 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 解决方法
refined中的Greater谓词支持Shapeless的类型级自然数(Nat)和整数单例类型(由Shapeless’s 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 尽管如此,这仍然会使堆栈的大值变大,所以整数单例类型是你的情况. （编辑：李大同） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |