0

我正在关注LH 教程，并且坚持练习以改进过滤器函数的类型，如果使用具有唯一元素的列表调用，则输出也是具有唯一元素的唯一列表。

这是我正在使用的代码：

import Data.Set hiding (insert, partition, filter, split, elems)

{-@ measure elts @-}
elts        :: (Ord a) => [a] -> Set a
elts []     = empty
elts (x:xs) = singleton x `union` elts xs

{-@ measure unique @-}
unique        :: (Ord a) => [a] -> Bool
unique []     = True
unique (x:xs) = unique xs && not (member x (elts xs))

{-@ filter' :: (a -> Bool) -> xs:[a] -> { l:[a] | unique xs => unique l } @-}
filter' _ []   = []
filter' f (x:xs)
  | f x       = x : xs'
  | otherwise = xs'
  where
    xs'       = filter' f xs

但是，当让 LH 证明它时，LH 会抛出以下错误：

filter.hs:16:17-23: Error: Liquid Type Mismatch

 16 |   | f x       = x : xs'
                      ^^^^^^^

   Inferred type
     VV : {v : [a] | tail v == xs'
                     && head v == x
                     && listElts v == Set_cup (Set_sng x) (listElts xs')
                     && len v == 1 + len xs'
                     && Main.elts v == Set_cup (Set_sng x) (Main.elts xs')
                     && (Main.unique v <=> Main.unique xs'
                                           && not (Set_mem x (Main.elts xs')))
                     && len v >= 0}

   not a subtype of Required type
     VV : {VV : [a] | Main.unique ?a => Main.unique VV}

   In Context
     xs : {v : [a] | len v >= 0}

     xs' : {v : [a] | (Main.unique xs => Main.unique v)
                      && len v >= 0}

     x : a

     ?a : {?a : [a] | len ?a >= 0}

我已经尝试以不同的方式指定它，在细化中使用 if 并使用不同的细化类型，但似乎都不起作用......

你能指出我正确的方向吗？我仍然很难理解错误消息。据我了解，推断的类型包含它是唯一的信息，如果xs'是唯一的，所以在我看来，这应该是所需类型的子类型。

4

1 回答 1

1

抱歉耽搁了，我才看到这个！（我倾向于更密切地监视松弛通道。）错误消息基本上是说 LH 无法证明输出列表x:xs'确实是唯一的。具体来说，LH 无法知道x已经不是 的一个元素xs'。

现在，为什么不是x的元素xs'？因为

(1)x不是xsAND 的元素 (2)xs'是值的子集xs

如果输入列表是唯一的，LH 知道第一个属性。

但它不知道第二个。因此，如果您将其添加到输出中filter会有所帮助。

[顺便说一句，这是一个很好的问题；我会用提示更新教程]

于 2020-06-11T04:32:26.427 回答