問題タブ [liquid-haskell]

または のような関数を呼び出す既存のプログラムを簡単に移行できる、注釈付きのバリアントまたは Haskell Prelude はありますheadかlength?

レイジー キューに関するLiquidHaskell ケース スタディの最初の演習を実行しようとしています。

okHd失敗します:

okListエラー メッセージから、LHが空でないことを「認識」するのに十分な情報を LH に提供していないことは確かですが、それを修正する方法がわかりません。

事後条件(?)で明示的に伝えてみました:

しかし、これはうまくいきません:

私は Liquid-Haskell を使ってどんな種類のきちんとしたことができるかを確認するためにいくつかの実験を行っていますが、ちょっとした壁にぶつかりました。基本的な考え方は、一定の時間が経過すると有効期限が切れるアクセス トークンを必要とする関数がいくつかあるということです。トークンを関数の 1 つに渡す前に、トークンの有効性を確認するために、liquid-haskell を使用する方法を確認しようとしています。私の問題を示す最小限の作業バージョンを以下に作成しました。このファイルで Liquid を実行すると、次のエラーが発生します。

なぜこのエラーが表示され、私が試したすべてが失敗したのか理解できないようです。誰か助けてくれませんか？

また、time パッケージの currTime 関数を getCurrentTime 関数に置き換えたいと考えています。そうすれば、トークンのタイムスタンプを現在の時刻と比較できます。つまり、私の isExpired 関数のタイプは Token -> IO Bool になります。液体ハスケルを使用してもそれは可能でしょうか?

ありがとう！

スタックでビルドされ、GHC 8 が必要なプロジェクトがあります。GHC 8 が必要な場合、私のプロジェクトで Liquid Haskell を使用することは可能ですか? その場合、Liquid Haskell をインストールして実行するにはどうすればよいですか?

ありがとう！