函数"map"的正确约定是什么?在Liquid Haskell中? [英] What is the correct contract of the function "map" in Liquid Haskell?
本文介绍了函数"map"的正确约定是什么?在Liquid Haskell中?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我正在尝试解决LiquidHaskell的一些练习教程.所以,我这样写:
I am trying to solve some exercise from LiquidHaskell tutorial. So, I wrote this:
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错误格式):
But I'm getting an error (excuse, pls, this formatting, it's the original LH error format):
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
的正确合约"是什么?如何解决这个错误?以及应该如何读取/处理类似Main.Cons##lqdc##$select v == ds_d35c x
的消息?
What is the right "contract" of mymap
? How to fix this error? And how should be read/treated messages like Main.Cons##lqdc##$select v == ds_d35c x
?
推荐答案
我必须显式注释构造函数. 之后,它将使用LiquidHaskell进行编译.
I had to explicitly annotate the constructors. After that, it compiles with 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
这篇关于函数"map"的正确约定是什么?在Liquid Haskell中?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文