はじめに

Liquid Haskell で少しハマったのでメモとして残しておきます。

本来なら先に仕様を書いて実装を書くべきだと思いますが、今回の例は既存のコードにリファインメント型をつけるような場合を想定しています。

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

Liquid Haskell を気になってる人向けの記事です。

やりたいこと

データの挿入と更新操作を次のような型で表現します。

上記のデータ型を使って、次のような関数を定義します。

adjustBound 関数は以下のように動作します。

adjustBound のような関数でバグが無いことを確認するためには何をしたら良いでしょうか?

型は非常に強力ですが、値について何も教えてくれません。

バグの少ない世界を目指して

僕が Haskell を使う理由は、第一に 楽しい からです。そのため、「勉強しても就職する時に役に立たないでしょ?」などと言われても全く気になりません。(そもそも、就職するために勉強するわけじゃないですよね)

また Haskell を使えば、正しいソフトウェアを普通に作ることができます。また、hspec などで単体テストを書いたり、QuichCheck などでランダムテストを書くことで、過去に起こった問題を再発させないようにする努力や、バグを少なくするための取り組みが行われています。

しかしながら、個人的にはどれもまだ不安です。もしかしたら、チェックしてない部分にバグがあるんじゃないの・・・?

そんな心配性の方は Liquid Haskell (LH) を使いましょう!

型をより厳しく

最初に定義した Operation 型と adjustBound を再掲します。

とりあえず、現在のコードを LH にかけてみます。

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


**** DONE:  A-Normalization ****************************************************


**** DONE:  Extracted Core using GHC *******************************************


**** DONE:  Transformed Core ***************************************************

Working 100% [=================================================================]

**** DONE:  annotate ***********************************************************


**** RESULT: SAFE **************************************************************

RESULT: SAFE が表示されれば問題ありません!

入力を自然数に限定させよう

例えば lowerupper が自然数 (0含む) しか許容しないという仕様が与えられた時、どうしますか?

よくある対応としては、コメントにその旨を書いたり、テストを作ったりという作業になるでしょう。

Liquid Haskell では上記の仕様を 事前条件 として記述することができます。

NatPrelude で以下のように定義されています。つまり、0以上の Int のみを含むリファインメント型です。

これだけです。LH で結果を確かめてみましょう。

$ liquid LH.hs
...

**** RESULT: SAFE **************************************************************

SAFE ですね!

これでもう adjustBoundlowerupper0 以上の自然数でしか呼び出されていないことが示されました。

もう少し具体例

では、別のプログラマが adjustBound を利用した関数を作ったとしましょう。この関数自体に意味はないですが、LH を理解するためにはとても良い例だと思います。

この関数 f は、型が正しいため当然コンパイルできます。

$ stack repl -- LH.hs
> f
-49

けれども、僕らの仕様では adjustBoundlowerupper には自然数しか適用してはいけないはずです。

次に LH を実行してみましょう。

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


 LH.hs:18:25-28: Error: Liquid Type Mismatch

 18 | f = adjustBound Insert (-100) (-50) (-70)
                              ^^^^


   Inferred type
    VV : {v : Int | v == (-?a)
                    && v == ?b}

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

  In Context
    ?b : {?b : Int | ?b == (-?a)}

    ?a : {?a : Int | ?a == (100 : int)}


 LH.hs:18:32-34: Error: Liquid Type Mismatch

 18 | f = adjustBound Insert (-100) (-50) (-70)
                                     ^^^


   Inferred type
    VV : {v : Int | v == (-?b)
                    && v == ?a}

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

  In Context
    ?b : {?b : Int | ?b == (50 : int)}

    ?a : {?a : Int | ?a == (-?b)}

UNSAFE になりましたね。こういうことです。

つまり、自分たちが使っている範囲Liquid Haskell のリファインメント型について、正しく整合性が取れているのかということを判定しています。

戻り値の型も厳しくしよう!

先程、事前条件についてリファインメント型を書きました。

次は事後条件についてリファインメントを書きましょう!

同様に戻り値の型も自然数という仕様にします。

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

リファインメント型 (Refinement type) は 篩 (ふるい) 型 と訳されている本 (入門LiquidHaskell−篩型による静的コード解析−) もありますが、それは Haskell の型の値が条件によって ふるい 落とされて、新しい型 (リファインメント型) になっているというイメージから来ているのだと思います。(読んだこと無いので間違ってたらすみません・・・。)

追記: チェシャ猫さんから 篩型 について教えてもらいました!

もっと仕様を

adjustBound 関数はこれで十分なのでしょうか?人によっては十分だね。と答えるかもしれません。

しかし、今回は次のような仕様を与えることにします。

  1. upperlower 以上の自然数
  2. Insert の操作の場合の戻り値は lowerupper + 1 の間の自然数
  3. Update の操作の場合の戻り値は lowerlower `max` (n `min` upper) の間の自然数

ここからが面白いところです。

まずは前準備として x 〜 y までの間の自然数を表すリファインメント型と述語を定義します。

では、仕様1を反映させてみましょう。

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

では次に、仕様2仕様3 です。

リファインメント型は以下のようになります。

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

はまったポイント

if (isInsert op) then (BtwnP l (u+1)) else BtwnP l u の部分でかなりはまりました。

例えば if の括弧を外した場合は次のようなエラーになります。

if isInsert op then (BtwnP l (u+1)) else BtwnP l u

**** RESULT: ERROR *************************************************************


 LH.hs:10:73: Error: Cannot parse specification:

 10 | {-@ adjustBound :: op:Operation -> l:Nat -> {u:Nat | l <= u}  -> _ -> {v:Nat | if isInsert op then (BtwnP l (u+1)) else BtwnP l u } @-}
                                                                              ^

     unexpected ":"
     expecting operator, white space or "}"

また、同様に then の括弧を外してもエラーになります。

if (isInsert op) then BtwnP l (u+1) else BtwnP l u

**** RESULT: ERROR *************************************************************


 LH.hs:10:73: Error: Cannot parse specification:

 10 | {-@ adjustBound :: op:Operation -> l:Nat -> {u:Nat | l <= u}  -> _ -> {v:Nat | if (isInsert op) then BtwnP l (u+1) else BtwnP l u } @-}
                                                                              ^

     unexpected ":"
     expecting operator, white space or "}"

else については括弧があっても無くても SAFE です。

この挙動が本当にわからなくてつらかったです・・・。

ちなみに、以下のような場合も同様にはまるので、ご注意ください。

-- UNSAFE
{-@ adjustBound :: _ -> l:Nat -> {u:Nat | l <= u}  -> _ -> Btwn l (u+1) @-}
{-@ adjustBound :: _ -> l:Nat -> {u:Nat | l <= u}  -> _ -> Btwn l {u+1} @-}

-- SAFE
{-@ adjustBound :: _ -> l:Nat -> {u:Nat | l <= u}  -> _ -> Btwn {l} {u+1} @-}

まとめ

  • if を使う場合は多めに括弧を付けておいた方が良さそう。
  • {} で囲むと上手くいく場合もある
  • LiquidHaskell はすごい

この良くわからない挙動について一緒に考えてくれた友人の tkg さんありがとうございました。

以上です。