gpt4 book ai didi

haskell - 如何使用 LiquidHaskell 指定对非空数据结构进行操作的函数?

转载 作者:行者123 更新时间:2023-12-01 23:31:06 25 4
gpt4 key购买 nike

我正尝试在 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 提供足够的信息以使其“知道”okList 是非空的,但我不知道如何修复它。

我试着用后置条件(?)明确地告诉它:

{-@ 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 分别定义了 okListSList 的细化类型只 promise size v = realSize (elems v),调用构造函数时会检查列表的大小,与数字字面量和然后丢弃,不存储在(液体)类型级别。因此,当您将 okList 提供给 hd 时,唯一可用于推理的信息是 size v = realSize (elems v)(来自精化数据类型) 和 size v >= 0(size 定义为 Nat),hd 不知道是否这是积极的。

hd okList 中,liquidhaskell 可能无法计算表达式,因此将 okList 替换为 Sl 1 ["cat"] 并获得有关大小的信息,因此它只能根据它推断出的 okList 的细化类型(在本例中为 SList String)进行判断。一个证据是 hd $ SL 1 ["cat"] 将在没有优化类型的情况下工作。

关于haskell - 如何使用 LiquidHaskell 指定对非空数据结构进行操作的函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/35544348/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com