如何使用 LiquidHaskell 指定对非空数据结构进行操作的函数?
How to specify a function operating on non-empty data structure with LiquidHaskell?
我正在尝试在 LiquidHaskell 中做第一个练习 case study on Lazy Queues
module Main where
main :: IO ()
main = putStrLn "hello"
{-@ type Nat = {v:Int | 0 <= v} @-}
{-@ die :: {v:String | false} -> a @-}
die x = error x
{-@ measure realSize @-}
realSize :: [a] -> Int
realSize [] = 0
realSize (_:xs) = 1 + realSize xs
{-@ data SList a = SL {
size :: Nat
, elems :: {v:[a] | realSize v = size}
}
@-}
data SList a = SL { size :: Int, elems :: [a]}
{-@ type NEList a = {v:SList a | 0 < size v} @-}
{-@ hd :: NEList a -> a @-}
hd (SL _ (x:_)) = x
hd _ = die "empty SList"
okList = SL 1 ["cat"]
okHd = hd okList
okHd
失败:
app/Main.hs:30:13-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : (SList [Char]) | VV == Main.okList}
not a subtype of Required type
VV : {VV : (SList [Char]) | 0 < size VV}
In Context
VV : {VV : (SList [Char]) | VV == Main.okList}
Main.okList
: (SList [Char])
根据错误消息,我很确定我没有向 LH 提供足够的信息以使其 "know" okList
是非空的,但我无法弄清楚如何修复它。
我试着用 post-condition(?) 明确地告诉它:
{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]
但这行不通:
app/Main.hs:29:5: Error: Specified Type Does Not Refine Haskell Type for Main.okList
Haskell: Main.SList [GHC.Types.Char]
Liquid : forall a. Main.SList a
您okList
的细化类型不限制类型。它限制了大小但将类型从 String
松散到 a
.
改变
{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]
至
{-@ okList :: NEList String @-}
okList = SL 1 ["cat"]
它会起作用。
我不得不承认我对 liquidhaskell 不是很了解所以下面的一切可能只是我的胡乱猜测:
您必须这样做的主要原因是您使用默认构造函数 SL
单独定义 okList
。 SList
的精化类型只承诺 size v = realSize (elems v)
,调用构造函数时会检查列表的大小,与数字文字进行比较然后丢弃,而不是存储在(液体)类型级别。因此,当您将 okList
提供给 hd
时,唯一可用于推理的信息是 size v = realSize (elems v)
(来自精化数据类型)和 size v >= 0
(size
被定义为a Nat
), hd
不知道是不是阳性
在hd okList
中,liquidhaskell可能无法计算表达式,因此将okList
替换为Sl 1 ["cat"]
并获得有关大小的信息,因此它只能进行判断取决于它推断出的 okList
的精化类型(在本例中为 SList String
)。一个证据是 hd $ SL 1 ["cat"]
将适用于没有改进的类型。
我正在尝试在 LiquidHaskell 中做第一个练习 case study on Lazy Queues
module Main where
main :: IO ()
main = putStrLn "hello"
{-@ type Nat = {v:Int | 0 <= v} @-}
{-@ die :: {v:String | false} -> a @-}
die x = error x
{-@ measure realSize @-}
realSize :: [a] -> Int
realSize [] = 0
realSize (_:xs) = 1 + realSize xs
{-@ data SList a = SL {
size :: Nat
, elems :: {v:[a] | realSize v = size}
}
@-}
data SList a = SL { size :: Int, elems :: [a]}
{-@ type NEList a = {v:SList a | 0 < size v} @-}
{-@ hd :: NEList a -> a @-}
hd (SL _ (x:_)) = x
hd _ = die "empty SList"
okList = SL 1 ["cat"]
okHd = hd okList
okHd
失败:
app/Main.hs:30:13-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : (SList [Char]) | VV == Main.okList}
not a subtype of Required type
VV : {VV : (SList [Char]) | 0 < size VV}
In Context
VV : {VV : (SList [Char]) | VV == Main.okList}
Main.okList
: (SList [Char])
根据错误消息,我很确定我没有向 LH 提供足够的信息以使其 "know" okList
是非空的,但我无法弄清楚如何修复它。
我试着用 post-condition(?) 明确地告诉它:
{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]
但这行不通:
app/Main.hs:29:5: Error: Specified Type Does Not Refine Haskell Type for Main.okList
Haskell: Main.SList [GHC.Types.Char]
Liquid : forall a. Main.SList a
您okList
的细化类型不限制类型。它限制了大小但将类型从 String
松散到 a
.
改变
{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]
至
{-@ okList :: NEList String @-}
okList = SL 1 ["cat"]
它会起作用。
我不得不承认我对 liquidhaskell 不是很了解所以下面的一切可能只是我的胡乱猜测:
您必须这样做的主要原因是您使用默认构造函数 SL
单独定义 okList
。 SList
的精化类型只承诺 size v = realSize (elems v)
,调用构造函数时会检查列表的大小,与数字文字进行比较然后丢弃,而不是存储在(液体)类型级别。因此,当您将 okList
提供给 hd
时,唯一可用于推理的信息是 size v = realSize (elems v)
(来自精化数据类型)和 size v >= 0
(size
被定义为a Nat
), hd
不知道是不是阳性
在hd okList
中,liquidhaskell可能无法计算表达式,因此将okList
替换为Sl 1 ["cat"]
并获得有关大小的信息,因此它只能进行判断取决于它推断出的 okList
的精化类型(在本例中为 SList String
)。一个证据是 hd $ SL 1 ["cat"]
将适用于没有改进的类型。