3

私は Liquid-Haskell を使ってどんな種類のきちんとしたことができるかを確認するためにいくつかの実験を行っていますが、ちょっとした壁にぶつかりました。基本的な考え方は、一定の時間が経過すると有効期限が切れるアクセス トークンを必要とする関数がいくつかあるということです。トークンを関数の 1 つに渡す前に、トークンの有効性を確認するために、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 パッケージの 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最後に、内部で使用するようにコードを書き直すことはできますが、現在の時刻は決してエスケープしないため、isValidおそらく の定義を変更する必要があります。これが私がそれを行う方法です。ValidTokenisValid

呼び出される「解釈されない」メジャー (本体なし) を定義し、のタイプを return にvalid変更します。残念ながら、LiquidHaskell は の定義を検証できません。したがって、 の型を使用して、信頼できるコンピューティング ベースの一部にする必要があります。これは小さな関数であり、想定する必要がある唯一のものであるため、これで問題ありません。isExpiredIO {v:Bool | ((Prop v) <=> (not (valid t)))}isExpiredvalidassumeisExpired

于 2016-08-14T14:18:24.083 に答える