如何使用withSizedList函数？

Question

我知道这是一个有点模糊的问题，但我试图找到答案，但找不到。

\n

任何人都可以提供一个关于如何使用包中的函数withSizedListvector-sized的合理示例吗？

\n

上下文是我正在构建一些法国套牌包。我决定用这个进行类型级编程，从vector...vector-sized显然，我的所有代码在更改后都崩溃了，但我设法修复了它，除了测试套件。我有一些quickcheck测试检查诸如sort (shuffle deck) == sort deck.

\n

这对于常规来说非常简单，vector因为您可以Arbitrary为 制作实例Card，然后为quickcheck提供实例[Card]；最后你只需编写一个像这样的属性，deck -> let vdeck = V.fromList deck ...这几乎是不可能的，因为编译时大小未知......显然，这可以通过文档中的vector-sized函数来克服withSizedList

\n

\n

将列表转换为具有适当大小参数的向量（在运行时确定）

\n

\n

（咆哮）问题是我无法使用这样的函数找到反向依赖关系，并且类型签名更像是埃及的 Jerogliphic，而不是实际有用的信息（咆哮）。我想说使用它的方式是这样的

\n

-- within the conext of defining a quickcheck property. Card has a good Arbitrary instance\n-- shuffle :: KnownNat n => Vector n Card -> Vector n Card (there is a random generator irrelevant for the example)\n-- sort :: KnownNat n => Vector n Card -> Vector n Card\n\nprop $ \\(deck :: [Card]) -> \n   let shuffled_sized_deck = deck `VSized.withSizedList` shuffle\n       sorted_sized_deck   = deck `VSized.withSizedList` sort\n    in sort shuffled_sized_deck == sorted_sized_deck\n\n\n-- In case you wonder, shuffle is implemented using withVectorUnsafe so\n-- the type (Vector n) doesn\'t guarantee they have the same length\n

\n

但我得到了错误

\n

\xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98r\xe2\x80\x99 with \xe2\x80\x98Vector n \xe2\x80\x99\n  Expected: V.Vector n Card -> r\n   Actual: V.Vector n Card -> V.Vector n Card\n

\n

那么...为什么不呢r ~ V.Vector n Card？我希望这个问题得到很好的解释。类型级编程让我很头疼，我不知道这个问题是否愚蠢。

\n

Answer 1

从概念上讲，该函数的类型是

\n

sizedList :: \xe2\x88\x80 a . [a] -> (\xe2\x88\x83 n. KnownNat n => Vector n a)  -- not legal Haskell\n

\n

即，它给出了一个先验未知的长度向量，或者换句话说：将存在一个数字，n使得返回向量的类型为n。

\n

Haskell 没有这样的存在类型，至少不是匿名的，你需要单独定义它：

\n

data DynVector a where\n  DynVector :: Vector n a -> DynVector a\n\nsizedList :: [a] -> DynVector a\n

\n

动态使用存在类型的标准技巧是应用连续传递扩展。你总是可以将一个函数转换f :: A -> B为一个函数

\n

fCPS :: \xe2\x88\x80 r . A -> (B -> r) -> r\nfCPS x \xcf\x86 = \xcf\x86 (f x)\n

\n

反之亦然，您可以检索原始表格

\n

f' :: A -> B\nf' x = fCPS x id\n

\n

或者

\n

f' x = x `fCPS` \\y -> y\n

\n

对于像这样的单态函数来说f，这只是一种使签名变得更加复杂的愚蠢方法，但是对于类似的东西，sizedList它具有将\xe2\x88\x83量量从协变位置（函数的结果）移动到逆变位置（函数的参数）的效果。继续\xcf\x86）。这种变化将存在量化量变成了通用量量。

\n

呃，呃……什么？

\n

看，返回某个长度的sizedList向量。这相当于说无论谁接受这个向量（即延续）都必须能够处理任何长度的输入。IOW，延续必须是长度上的多态函数。这正是签名的内容

\n

withSizedList :: \xe2\x88\x80 a r . [a] -> (\xe2\x88\x80 n . KnownNat n => Vector n a -> r) -> r\nwithSizedList \xcf\x86 l = \xcf\x86 (sizedList l)\n          -- N.B. this can NOT be written  \xcf\x86 $ sizedList l\n

\n

表示。

\n

那么如何使用它呢？实际上你尝试的很接近，但问题是具体的类型值n无法逃脱它必须始终是的延续 \xe2\x80\x93 r，它可以是任何类型，但需要预先选择。然而，结果deck `VSized.withSizedList` sort再次需要是一个存在类型，即使支持这一点，也无济于事，因为它deck `VSized.withSizedList` shuffle会给出另一个存在值，类型系统无法知道它们都具有相同的值长度。

\n

您需要选择的类型r是整个计算的最终结果，即简单的Bool。这意味着您需要将处理多态长度的所有内容包装到一个单一的延续中，而不是拥有多个单独的延续：

\n

prop $ \\(deck :: [Card]) -> deck `VSized.withSizedList` \\deckV ->\n          shuffle deckV == sort deckV\n

\n

或更短

\n

prop (`VSized.withSizedList` \\deck -> shuffle deck == sort deck)\n

\n