固定大小和元素边界的 Nat 列表

Question

使用 shapeless，我正在尝试定义一个函数：

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 个元素（如果可能）。

Answer 1

您输入的签名是 List，大小为 N，仅包含 N 类型的元素。也就是说，Sized[List[N], N] 表示以下之一：List(_1)、List(_2, _2) 或最后 List(_3, _3, _3)，考虑到您的类型级别约束。这几乎就是您想要的，并解释了编译器给您的错误：

required: shapeless.Sized[List[shapeless.nat._3],shapeless.nat._3]

要开始分解您想要完成的任务，我们需要注意您不能在拥有 List[Nat] 的同时保留各个类型。 Nat 的抽象性会使它们模糊不清。所以如果你想在编译时做一些事情，你将有三个选择：使用 HList，选择在列表中修复 Nat 的类型，这样你就有 List[N] 或选择用 Sized.

固定 List[Nat] 的大小

如果你想说 List 的尺寸小于 3，那么

def lessThanThree[N <: Nat](sz: Sized[List[Nat], N])(implicit ev: LTEq[N, _3]) = sz

如果你想说 List 的 Nat 小于三，再次在 List 内固定 N:

def lessThanThree[N <: Nat, M <: Nat](sz: Sized[List[N], M])(implicit ev: LTEq[N, _3]) = sz

如果您希望使用 Poly 工作，您可以在其中为任何 Nat 定义 at 以保留 LTEq 约束，您需要了解 Sized 确实使使用 map 更接近大多数集合中的标准包 map，即它需要 CanBuildFrom。这与 List 中个人 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，同时也只允许 HList 包含小于或等于 3 的 Nat。

固定大小和元素边界的 Nat 列表

List of Nat of Fixed Size and Element Bounds

scala

shapeless