LiquidHaskell
一応Logically Qualified Data Haskellの略らしい
Haskellで篩型をする
既存Haskellのプロジェクトに部分的に導入することもできる
バックエンドとしてZ3を使用する
フロントエンド
こっちを使う
バックエンドのSMTに投げるための処理などをしている
オンライン実行環境
コメント
{-@ .. @-} を用いてHaskellコードにannotionをつけるhs{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead :: [a] -> a
safeHead [] = liquidError "empty list"
safeHead (x : _) = x篩型エイリアスの定義が可能
hs{-@ type Pos = { v:Int | v > 0 } @-}上の方に↑を定義しておけば、別の場所で↓のように使える
hs{-@ hoge :: Pos @-}
hoge ..参考