3

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

/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 函数替换为 getCurrentTime 函数。这样我就可以将令牌上的时间戳与当前时间进行比较。这意味着我的 isExpired 函数将是 Token -> IO Bool 类型。这甚至可以使用液体哈斯克尔吗？

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

谢谢！

4

1 回答 1

1

这里有几个问题。

  1. 您试图将其定义currTime为度量，但度量应该是函数。这应该被 LiquidHaskell 标记为错误。

  2. 在进行度量之前，您可能已经注意到这一点currTime，但您目前无法在类型签名中引用顶级定义。我们可以通过currTime作为参数传递给isExpired，并通过向ValidToken类型添加参数来修复您的示例（这可能是您无论如何都想要做的，因为令牌的有效性与某个时间戳有关）。这是我们演示页面上工作版本的链接。

最后，您当然可以重写代码以getCurrentTime在 inside中使用isValid，尽管您可能需要更改 的定义，ValidToken因为当前时间永远不会转义isValid。这就是我将如何做到的。

我定义了一个名为“未解释”的度量（无主体）valid并将isExpired's 的类型更改为 return IO {v:Bool | ((Prop v) <=> (not (valid t)))}。不幸的是，LiquidHaskell 无法验证 的定义，isExpired因为我们还没有告诉它是什么valid意思。所以我们必须为assume的类型isExpired，使其成为我们可信计算库的一部分。我对此很满意，因为它是一个小功能，并且是唯一需要假设的事情。

于 2016-08-14T14:18:24.083 回答