使用无形,我正在尝试定义一个函数:
import shapeless._
import ops.nat._
import nat._
def threeNatsLessThan3[N <: Nat](xs: Sized[List[N], N])
(implicit ev: LTEq[N, _3]) = ???
只有当输入xs是Nat的List(大小为3)时,它才会编译,其中每个元素都是< = 3. 但是无法编译:
scala> threeNatsLessThan3[_3](List(_1,_2,_3))
<console>:22: error: type mismatch;
found : List[shapeless.Succ[_ >: shapeless.Succ[shapeless.Succ[shapeless._0]] with shapeless.Succ[shapeless._0] with shapeless._0 <: Serializable with shapeless.Nat]]
required: shapeless.Sized[List[shapeless.nat._3],shapeless.nat._3]
(which expands to) shapeless.Sized[List[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]],shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]]a>
twoNatsFirstLtEqSecond[_3](List(_1,_2,_3))
^
如何正确实现上述功能?
此外,我也很欣赏使用HList的解决方案,其中HList仅包含Nat元素(如果可能).
最佳答案 您输入的签名是大小为N的列表,其中仅包含N类型的元素.对于whit,Sized [List [N],N]表示以下之一:List(_1),List(_2,_2) ),或最后列出(_3,_3,_3),考虑到你的类型级别约束.这几乎就是你想要的,并解释了编译器给你的错误:
required: shapeless.Sized[List[shapeless.nat._3],shapeless.nat._3]
要开始分解您想要完成的任务,我们需要注意您不能拥有List [Nat]并保留各个类型. Nat的抽象性会使他们模糊不清.因此,如果你想在编译时做一些事情,你将有三个选择:使用HList,选择在列表中修复Nat的类型,以便你有List [N]或选择修复大小列表[Nat]与大小.
如果你想说List的大小小于3,那么
def lessThanThree[N <: Nat](sz: Sized[List[Nat], N])(implicit ev: LTEq[N, _3]) = sz
如果你想说List的Nat小于3,那么List中的N也是固定的:
def lessThanThree[N <: Nat, M <: Nat](sz: Sized[List[N], M])(implicit ev: LTEq[N, _3]) = sz
如果您正在寻找可能使用Poly,您可以为任何Nat定义一个at以保留LTEq约束,您需要了解Sized确实使得地图符合更接近于上面的标准包映射大多数集合,即它需要CanBuildFrom.结合列表中的个体Nat的擦除意味着您将遇到很多困难,提出一种解决方案,为您提供所需的灵活性.
如果您使用HList,则可以执行以下操作:
object LT3Identity extends Poly{
implicit def only[N <: Nat](implicit ev: LTEq[N, _3]) = at[N]{ i => i}
}
def lt3[L <: HList, M <: Nat](ls: L)(implicit lg: Length.Aux[L, M], lt: LTEq[M, _3]) = ls.map(LT3Identity)
这样做既可以将Hlist的大小限制为小于3,同时也只允许包含小于或等于3的Nat的HList.