如何使用vector-sized包的withSizedList函数（QuickCheck测试场景）

问题背景 #

我正在开发法式扑克牌的Haskell包，为了用类型级编程约束容器大小，从普通vector迁移到vector-sized。大部分代码都修复完成，但QuickCheck测试卡壳了——比如要验证sort (shuffle deck) == sort deck这个属性。

用普通vector时很简单：给Card实现Arbitrary实例，QuickCheck自动生成[Card]实例，转成Vector即可。但vector-sized的大小是编译期确定的，测试时运行期生成的列表长度没法直接对应。看到withSizedList的文档说明它能「将列表转换为具有适当大小参数的向量，大小由运行时决定」，但找不到示例，自己写的代码报错了。

错误代码与报错信息 #

我尝试的代码：

-- 上下文：定义QuickCheck属性，Card已实现合法的Arbitrary实例
-- shuffle :: KnownNat n => Vector n Card -> Vector n Card（随机生成器细节不影响示例）
-- sort :: KnownNat n => Vector n Card -> Vector n Card

prop $ \(deck :: [Card]) -> 
   let shuffled_sized_deck = deck `VSized.withSizedList` shuffle
       sorted_sized_deck   = deck `VSized.withSizedList` sort
    in sort shuffled_sized_deck == sorted_sized_deck

-- 补充：shuffle用了withVectorUnsafe实现，所以Vector n类型不能保证长度一致

报错信息：

• Couldn't match type ‘r’ with ‘Vector n ’
  Expected: V.Vector n Card -> r
   Actual: V.Vector n Card -> V.Vector n Card

问题分析 #

withSizedList的类型签名是withSizedList :: [a] -> (forall n. KnownNat n => Vector n a -> r) -> r，核心逻辑是：

• 运行时读取列表长度，绑定到类型级自然数n
• 回调函数必须能接受任意满足KnownNat n的n，且返回值r不能依赖n

你之前的写法错误在于，试图让withSizedList直接返回Vector n Card——但Vector n Card依赖于n，不符合r必须与n无关的要求（属性测试最终需要返回Bool，这才是合法的r）。

解决方案 #

正确的做法是把整个属性测试逻辑放进withSizedList的回调函数中，让所有依赖KnownNat n的操作都在n绑定的作用域内完成，最后返回不依赖n的Bool结果。

修改后的代码：

import qualified Data.Vector.Sized as VSized
import Test.QuickCheck

-- 假设Card的Arbitrary实例已正确定义
-- shuffle, sort的类型保持不变：KnownNat n => Vector n Card -> Vector n Card

prop_shuffle_preserves_elements :: Property
prop_shuffle_preserves_elements =
  forAll (arbitrary :: Gen [Card]) $ \deck ->
    VSized.withSizedList deck $ \(vdeck :: VSized.Vector n Card) ->
      let shuffled = shuffle vdeck
          sorted_shuffled = sort shuffled
          sorted_original = sort vdeck
      in sorted_shuffled == sorted_original

额外建议 #

因为你的shuffle用了withVectorUnsafe，Vector n的类型约束无法保证长度不变，建议在测试中额外验证长度：

in VSized.length shuffled == VSized.length vdeck && sorted_shuffled == sorted_original

内容的提问来源于stack exchange，提问作者lsmor