LiquidHaskell - mrsekut-p

LiquidHaskell

https://github.com/ucsd-progsys/liquidhaskell/raw/develop/resources/logo.png

一応Logically Qualified Data Haskellの略らしい

Haskellで篩型をする

既存Haskellのプロジェクトに部分的に導入することもできる

バックエンドとしてZ3を使用する

github/liquidhaskell

フロントエンド

こっちを使う

github/liquid-fixpoint

バックエンドのSMTに投げるための処理などをしている

オンライン実行環境

コメント{-@ .. @-}を用いてHaskellコードにannotionをつける

code:hs

{-@ safeHead :: { xs:a | len xs > 0 } -> a @-}

safeHead :: a -> a

safeHead [] = liquidError "empty list"

safeHead (x : _) = x

篩型エイリアスの定義が可能

code:hs

{-@ type Pos = { v:Int | v > 0 } @-}

上の方に↑を定義しておけば、別の場所で↓のように使える

code:hs

{-@ hoge :: Pos @-}

hoge ..

参考

http://goto.ucsd.edu/~nvazou/real_world_liquid.pdf

『An Introduction to LiquidHaskell』

https://ucsd-progsys.github.io/liquidhaskell-tutorial/

https://ccvanishing.hateblo.jp/entry/2016/12/24/193038

https://forestaa.github.io/blog/posts/liquidhaskell1/

https://forestaa.github.io/blog/posts/liquidhaskell2/

https://forestaa.github.io/blog/posts/liquidhaskell3/

https://forestaa.github.io/blog/posts/liquidhaskell4/

https://www.slideshare.net/y_taka_23/liquid-haskell-ngk2017b-83162127

https://7colou.red/blog/2018/07-07-difference/index.html

http://www.fos.kuis.kyoto-u.ac.jp/~t-sekiym/papers/ja/rech/main.pdf