はじめに

Liquid Haskell を半年ほど勉強した結果、色々と出来ることが増えて楽しくなってきました。

現状、日本語で詳しく説明しているブログ記事や Qiita 記事はほとんどありません。

とても面白いツールだと思いますので、色々と紹介していけたらと思います。

今回は Liquid Haskell の導入方法について簡単に説明したいと思います。

Liquid Haskell とは?

Liquid HaskellGHC の型よりも、さらに厳密な 篩型 (Refinement Type) の型検査器です。

既存のコードを変更 (さらには実行すら) することなく利用できるため、既存のプロジェクトの一部にだけ導入することも可能です。

また、つい最近も GADT をサポートしたりと、開発はとても活発に行われています。

正しいソフトウェアを楽しく作るために、Liquid Haskell を学習してみるのはどうでしょうか!

ちなみに Liquid という単語は 液体 と言いたくなりますが、それとはあまり関係なく、実際は Logically Qualified Data の略です。(ロゴは 水滴 + >>= なので、全く無関係では無いかもですが)

インストール

Liquid Haskell は以下の2つのリポジトリで開発が進められています。

liquidhaskell がフロントエンド (コマンドライン処理やパーサーなどの処理等) を行い liquid-fixpointSMT ソルバに投げるための処理を色々とやっている印象です。(詳しくないので間違ってたらすみません)

なので、僕らが関係するのは基本的に liquidhaskell リポジトリの方です。(liquid-fixpoint はサブモジュールになっています)

また、実際にチェックを行うのは SMT ソルバなので、そちらも同様にインストールが必要です。

SMT ソルバのインストール

SMT ソルバも色々と種類があるようで、公式では以下の3種類が紹介されています。

  • Z3
  • CVC4
  • MathSat

どれでもちゃんと動くので好きなソルバを使えば良いのですが、どれを選んだら良いかわからない人は Z3 にしましょう。

理由としてはインストール方法が簡単で、性能も良いそうです。

Ubuntu

$ sudo apt install z3

$ z3 --version
Z3 version 4.4.1

Mac (brew)

$ brew install z3

$ z3 --version
Z3 version 4.6.0 - 64 bit

Liquid Haskell のインストール

現状、一番安定しているのは githubdevelop ブランチを stack でビルドしてインストールする方法だと思います。

また、その他のインストール方法等は INSTALL.md をご参照下さい。

$ git clone --recursive git@github.com:ucsd-progsys/liquidhaskell.git
$ cd liquidhaskell
$ stack install

$ liquid
LiquidHaskell Version 0.8.2.4, Git revision d641244775cd842776cecf2c5d3e9afa01549e76 (dirty)
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

stack プロジェクトで利用する場合は、以下のように stack exec コマンドで呼び出します。

$ stack exec -- liquid
LiquidHaskell Version 0.8.2.4, Git revision d641244775cd842776cecf2c5d3e9afa01549e76 (dirty)
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

サンプルプログラム

myDiv 関数の例を使って LiquidHaskell に慣れましょう!

myDiv の実装は単に div をラップしただけです。

この関数はだいたい上手く動きますが、もし第二引数に 0 が与えられたらどうでしょうか?そう、実行時エラーになります・・・。試してみましょう。

$ stack repl -- MyDiv.hs
*MyDiv> myDiv 10 2
5
*MyDiv> myDiv 10 0
*** Exception: divide by zero

全然安全ではありませんね。

では、どうしたら本当に安全な myDiv を作れるのでしょうか?

その答えは篩(ふるい)型にあります。

Liquid Haskell では 篩型{-@ ... @-} のコメント形式で記述します。Liquid Haskell を利用するメリットの1つは、篩型の自動推論です。(推論できない場合も多々ありますが、結構色々と推論してくれます)

先程の myDiv には篩型を書いていませんが、こういう場合に Liquid HaskellHaskell の型をそのまま篩型として利用します。

myDiv に対して明示的に篩型を書いてみましょう!

この myDiv 関数を LquidHaskell でチェックしてみましょう。

$ liquid MyDiv.hs
**** RESULT: UNSAFE ************************************************************

 MyDiv.hs:4:11-13: Error: Liquid Type Mismatch

 4 | myDiv = div
             ^^^

   Inferred type
     VV : Int

   not a subtype of Required type
     VV : {VV : Int | VV /= 0}

   In Context

なぜか UNSAFE が表示されましたね。これは Liquid Haskell で既に div の篩型が定義されているからです。(div 以外にも色々ありますが、充実しているとは言い難いと思います)

だいたいこんな感じで、第二引数に 0を含まないInt型 という事前条件がついているのです。

そのため、先程のエラーメッセージで以下のように指摘されてしまったのです。

not a subtype of Required type
     VV : {VV : Int | VV /= 0}

つまり、僕らの定義した篩型は 0 を含む Int 型なので、このままだと div0 が与えられてしまう可能性があるよ!ということを教えてくれています。

myDiv にも同じ篩型をつけてみましょう。

これで SAFE になります。

$ liquid MyDiv.hs
**** RESULT: SAFE **************************************************************

0 を含まない Int 型というのは、よく使いそうなので篩型のエイリアスとして定義してみます。

篩型のエイリアスは type キーワードを使います。Haskell と同じですね。

そして myDiv の篩型も NonZero で置き換えます。

意味は全く同じですが、先程よりもわかりやすくなりました。

$ liquid MyDiv.hs
**** RESULT: SAFE **************************************************************

最後に myDiv を呼び出す関数を定義してみましょう。

good は問題の無い使い方です。

しかし、以下のような関数 bad が定義された場合、Liquid HaskellUNSAFE を返します。

$ liquid MyDiv.hs
**** RESULT: UNSAFE ************************************************************

 MyDiv.hs:13:7-16: Error: Liquid Type Mismatch

 13 | bad = myDiv 10 0
            ^^^^^^^^^^

   Inferred type
     VV : {v : Int | v == (0 : int)
                     && v == ?a}

   not a subtype of Required type
     VV : {VV : Int | VV /= 0}

   In Context
     ?a : {?a : Int | ?a == (0 : int)}

問題

以下のプログラムは標準入力から入力された数 n, msafeDiv n m を計算します。

safeDivcheck を正しく実装して Liquid Haskell の結果を SAFE にしてみましょう。

Hint: div0 を通さないよう check でバリデーションすれば良いです。

エラーメッセージ

現状では、Liquid Haskell は以下のエラーメッセージを返します。

$ liquid Main.hs
**** RESULT: UNSAFE ************************************************************

 Main.hs:24:24-30: Error: Liquid Type Mismatch

 24 |   | check     = Just $ div n m
                             ^^^^^^^

   Inferred type
     VV : {v : Int | v == m}

   not a subtype of Required type
     VV : {VV : Int | VV /= 0}

   In Context
     m : Int

実行例

Liquid HaskellUNSAFE の場合は実行時エラーが発生します。

$ stack repl -- Main.hs
*Main> main
10
2
5

*Main> main
10
0
*** Exception: divide by zero

Liquid HaskellSAFE にすると、再入力を促すようになります。

*Main> main
10
0
第二引数に0が入力されています
もう一度入力してください
10
2
5

興味を持った方へ

Liquid Haskell に興味を持った方は以下の文献を読んで Liquid Haskell に詳しくなりましょう!(個人的にまとめているやつを貼り付けただけなので雑ですみません・・・)

たぶん、おすすめは以下のチュートリアルです。(僕はまだ読んでないですが、かなり最近できたものなので情報が新しく良いのではないかと思います)

日本語の情報

ブログ

チュートリアル

スライド

  1. Liquid Types For Haskell
  2. Simple Refinement Types
  3. Measuring Data Types
  4. Higher-Order Specifications
  5. Abstract Refinements
  6. Lazy Evaluation?
  7. Refinements & Termination
  8. Evaluation

論文

Youtube

まとめ

  • 篩型は {-@ ... @-} で記述する
  • 篩型の型エイリアスは {-@ type @-} で記述する

以上です。