haskell - Liquid Haskell中函数 "map"的正确协定是什么？

我正在尝试解决LiquidHaskell tutorial的一些练习。所以，我这样写:

data List a = Nil | Cons a (List a) deriving (Show)
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` xs) = f x `Cons` mymap f xs

但是我遇到了一个错误(请问，这种格式，它是原始的LH错误格式):

53 | mymap f (x `Cons` xs) = f x `Cons` mymap f xs
                              ^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : (Main.List a) | Main.Cons##lqdc##$select v == ?a
                               && Main.Cons##lqdc##$select v == ds_d35c x
                               && v == Main.Cons (ds_d35c x) ?a}

   not a subtype of Required type
     VV : {VV : (Main.List a) | len ?b == len VV}

   In Context
     xs : (Main.List a)

     ?b : (Main.List a)

     x : a

     ?a : {?a : (Main.List a) | len xs == len ?a}

mymap的正确“契约(Contract)”是什么？如何解决这个错误？以及应该如何阅读/处理诸如Main.Cons##lqdc##$select v == ds_d35c x的消息？

最佳答案

我必须显式注释构造函数。
之后，它将使用LiquidHaskell进行编译。

data List a = Nil | Cons a (List a) deriving (Show)
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ Nil   ::  { ys : List a | len ys == 0 } @-}
{-@ Cons  ::  a -> xs : List a -> { ys : List a | len ys == 1 + len xs } @-}

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } / [ len xs ] @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` xs) = f x `Cons` mymap f xs

关于haskell - Liquid Haskell中函数 "map"的正确协定是什么？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/56326273/