使用Liquid Haskell检查有效令牌

Question

我正在使用Liquid Haskell进行一些实验，看看能用它做些什么有趣的事情，但是我遇到了一些问题。基本思路是，我有一些需要访问令牌的函数，当令牌过期后就无法使用。我想尝试使用Liquid Haskell确保在将令牌传递给其中一个函数之前检查其有效性。下面是一个演示我的问题的最小化工作版本。当我在这个文件上运行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}

我似乎无法弄清为什么会出现这个错误，我尝试过的一切都失败了。请有人帮帮我吗？

另外，我想用time包中的getCurrentTime函数替换currTime函数。这样我就可以将令牌上的时间戳与当前时间进行比较。那么我的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

谢谢！

- ulbrec

Answer 1

这里有几个问题。

1. 你试图将 currTime 定义为一个度量，但是度量应该是函数。LiquidHaskell 应该会标记这个错误。

2. 在你将 currTime 定义为度量之前可能已经注意到了，但是你目前不能在类型签名中引用顶层定义。我们可以通过将 currTime 作为参数传递给 isExpired，并向 ValidToken 类型添加一个参数来修复你的示例（这也是你想要做的，因为令牌的有效性是针对某个时间戳的）。这里有一个 link 指向我们演示页面上的工作版本。

最后，你可以重写代码，在isValid中使用getCurrentTime，不过你可能需要改变ValidToken的定义，因为当前时间永远不会逃离isValid。这里是我会怎么做。

我定义了一个“未解释”的度量（没有身体），称为valid，并将isExpired的类型更改为返回IO {v：Bool |（（Prop v）<=>（not（valid t））)}。不幸的是，LiquidHaskell无法验证isExpired的定义，因为我们没有告诉它valid的含义。因此，我们必须assume isExpired的类型，使其成为我们信任的计算基础的一部分。我没问题，因为这是一个小函数，并且是唯一需要假定的事情。

- Eric Seidel

---

感谢您提供的出色答案和可工作演示的链接。这正是我所需要的。 - ulbrec