Liquid Haskell 中函数 "map" 的正确契约是什么?
What is the correct contract of the function "map" in Liquid Haskell?
我正在尝试解决来自 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"是什么?如何修复此错误? read/treated 消息应该如何 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
我正在尝试解决来自 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"是什么?如何修复此错误? read/treated 消息应该如何 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