使用液體哈斯克爾來檢查有效令牌

Question

我正在做一些使用液體哈斯克爾的實驗來看看我可以用它做什麼樣的整齊的事情，並且我碰到了一堵牆。基本思想是我有一些功能需要訪問令牌，在經過一段時間後過期。我試圖看看如何使用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} 

我似乎無法找出爲什麼這個錯誤被顯示出來，一切我曾嘗試已經失敗。有人可以幫我嗎？

此外，我想用時間包中的getCurrentTime函數替換currTime函數。這樣我可以比較令牌上的時間戳和當前時間。這意味着我的isExpired函數的類型是Token - > IO Bool。這甚至可以使用液體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類型添加一個參數來修復您的示例（由於令牌的有效性與某個時間戳有關，所以您可能希望這樣做）。以下是我們的演示頁面上工作版本的link。

最後，你當然可以重寫代碼使用getCurrentTime內isValid，雖然你可能需要改變的ValidToken的定義，因爲當前的時間從來沒有逃脫isValid。 Here's我該怎麼做。

我定義一個「未解釋的」測量（無體）稱爲valid和改變isExpired的類型返回IO {v:Bool | ((Prop v) <=> (not (valid t)))}。不幸的是，LiquidHaskell無法驗證isExpired的定義，因爲我們沒有告訴它valid的含義。所以我們必須assume類型爲isExpired，使它成爲我們可信計算基礎的一部分。我對此很滿意，因爲它是一個小功能，而且這是唯一需要假設的事情。