haskell - 使用 Liquid Haskell 检查有效 token

Question

我正在使用 liquid-haskell 做一些实验，看看我可以用它做些什么巧妙的事情，但我遇到了一些困难。基本思想是我有一些功能需要访问 token ，该 token 会在经过一定时间后过期。我正在尝试了解如何使用 liquid-haskell 来确保在将 token 传递到我的函数之一之前检查 token 的有效性。我在下面创建了一个最小的工作版本来演示我的问题。当我在此文件上运行 liquid 时，出现以下错误:

/tmp/liquidTest.hs:18:17-42: Error: Liquid Type Mismatch

 18 | isExpired tok = currTime >= expiration tok
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {VV : GHC.Types.Bool | Prop VV <=> Main.currTime >= ?a}

   not a subtype of Required type
     VV : {VV : GHC.Types.Bool | Prop VV <=> currTime >= expiration tok}

   In Context
     Main.currTime := Data.Time.Clock.UTC.UTCTime

     tok := Main.Token

     ?a := {?a : Data.Time.Clock.UTC.UTCTime | ?a == expiration tok}

我似乎无法弄清楚为什么会出现此错误，而且我尝试的一切都失败了。有人可以帮助我吗？

此外，我想将 currTime 函数替换为 time 包中的 getCurrentTime 函数。这样我就可以将 token 上的时间戳与当前时间进行比较。这意味着我的 isExpired 函数的类型为 Token -> IO Bool。这甚至可以使用 liquid haskell 吗？

import Data.Time
import Language.Haskell.Liquid.Prelude

{-@ data Token = Token
         (expiration :: UTCTime)
@-}

data Token = Token
    { expiration :: UTCTime
    } deriving Show

{-@ measure currTime :: UTCTime @-}
currTime :: UTCTime
currTime = UTCTime (ModifiedJulianDay 57614) 83924.978297

{-@ isExpired :: t:Token -> {v:Bool | ((Prop v) <=> (currTime >= expiration t))} @-}
isExpired :: Token -> Bool
isExpired tok = currTime >= expiration tok

{-@ type ValidToken = {t:Token | currTime < expiration t} @-}

{-@ showToken :: ValidToken -> String @-}
showToken :: Token -> String
showToken tok = show tok

main :: IO ()
main = do
  ct <- getCurrentTime
  let tok = Token ct

  print currTime

  case isExpired tok of
    True -> putStrLn "The token has expired!"
    False -> putStrLn $ showToken tok

谢谢!

Answer 1

这里有几个问题。

1. 您正在尝试定义 currTime作为一种措施，但措施应该是功能。这应该被 LiquidHaskell 标记为错误。

2. 在制作 currTime 之前您可能已经注意到了这一点一种措施，但您目前无法在类型签名中引用顶级定义。我们可以通过传递 currTime 来修复您的示例作为 isExpired 的参数, 并通过向 ValidToken 添加参数类型(这可能是你想要做的，因为 token 的有效性是关于某个时间戳的)。这是一个 link到我们演示页面上的工作版本。

最后，您当然可以重写代码以使用getCurrentTime里面isValid ，尽管您可能需要更改 ValidToken 的定义因为当前时间永远不会逃脱 isValid . Here's我会怎么做。

我定义了一个名为 valid 的“未解释”度量(无正文)并更改 isExpired要返回的类型 IO {v:Bool | ((Prop v) <=> (not (valid t)))} .不幸的是，LiquidHaskell 无法验证 isExpired 的定义因为我们还没有告诉它什么valid方法。所以我们必须 assume isExpired 的类型，使其成为我们可信赖的计算基础的一部分。我对此没有意见，因为它是一个小函数，而且是唯一需要假设的东西。