はじめに

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

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

$ liquid --version
LiquidHaskell Version 0.8.6.2 no git information
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

LiquidHaskell について気になってる人向けの記事です。

やりたいこと

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

data Operation = Insert | Update
  deriving Eq

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

adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n
  | isInsert op = upper + 1
  | otherwise   = lower `max` (n `min` upper)

isInsert :: Operation -> Bool
isInsert Insert = True
isInsert _      = False

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

> adjustBound Insert 0 10 5
11
> adjustBound Insert 0 10 100
11
> adjustBound Insert 0 10 (-100)
11

> adjustBound Update 0 10 5
5
> adjustBound Update 0 10 100
10
> adjustBound Update 0 10 (-100)
0

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

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

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

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

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

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

そんな心配性の方は LiquidHaskell (LH) に触れてみてください。

型をより厳しく

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

-- LH.hs
module LH where

data Operation = Insert | Update
  deriving Eq

adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n | isInsert op = upper + 1
                             | otherwise   = lower `max` (n `min` upper)

isInsert :: Operation -> Bool
isInsert Insert = True
isInsert _      = False

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

$ liquid LH.hs 
LiquidHaskell Version 0.8.6.2 no git information
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: LH.hs

**** [Checking: LH.hs] *********************************************************

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

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

**** DONE:  Transformed Core ***************************************************
 
Working 100% [=================================================================]

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

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

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

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

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

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

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

{-@ adjustBound :: _ -> Nat -> Nat -> _ -> _ @-}
adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n
  | isInsert op = upper + 1
  | otherwise   = lower `max` (n `min` upper)

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

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

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

$ liquid LH.hs
...

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

SAFE ですね!

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

もう少し具体例

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

f :: Int
f = adjustBound Insert (-100) (-50) (-70)

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

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

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

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

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

 LH.hs:17:24-29: Error: Liquid Type Mismatch
  
 17 | f = adjustBound Insert (-100) (-50) (-70)
                             ^^^^^^
  
   Inferred type
     VV : {v : GHC.Types.Int | v == (-100)}
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV >= 0}


 LH.hs:17:31-35: Error: Liquid Type Mismatch
  
 17 | f = adjustBound Insert (-100) (-50) (-70)
                                    ^^^^^
  
   Inferred type
     VV : {v : GHC.Types.Int | v == (-50)}
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV >= 0}

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

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

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

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

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

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

{-@ adjustBound :: _ -> Nat -> Nat -> _ -> Nat @-}
adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n | isInsert op = upper + 1
                             | otherwise   = lower `max` (n `min` upper)
$ liquid LH.hs
**** RESULT: SAFE **************************************************************

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

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

もっと仕様を

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

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

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

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

まずは前準備として xy までの間の自然数を表す述語を定義します。

{-@ predicate BtwnP Lo Hi V = Lo <= V && V <= Hi @-}

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

{-@ adjustBound :: _ -> l:Nat -> {u:Nat | l <= u} -> _ -> Nat @-}
adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n
  | isInsert op = upper + 1
  | otherwise   = lower `max` (n `min` upper)
$ liquid LH.hs
**** RESULT: SAFE **************************************************************

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

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

{-@ adjustBound ::
      op:Operation ->
      l:Nat ->
      {u:Nat | l <= u} ->
      _ ->
      {v:Nat | if (isInsert op) then (BtwnP l (u+1) v) else BtwnP l u v}
@-}
adjustBound :: Operation -> Int -> Int -> Int -> Int
adjustBound op lower upper n
  | isInsert op = upper + 1
  | otherwise   = lower `max` (n `min` upper)

{-@ measure isInsert @-}
isInsert :: Operation -> Bool
isInsert Insert = True
isInsert _      = False
$ liquid LH.hs
**** RESULT: SAFE **************************************************************

はまったポイント

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

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

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

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


 LH.hs:13:9: Error: Cannot parse specification:
  
 13 |       {v:Nat | if isInsert op then (BtwnP l (u+1) v) else BtwnP l u v}
              ^
  
     unexpected ":"
     expecting operator, white space or "}"

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

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

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


 /LH.hs:13:9: Error: Cannot parse specification:
  
 13 |       {v:Nat | if (isInsert op) then BtwnP l (u+1) v else BtwnP l u v}
              ^
  
     unexpected ":"
     expecting operator, white space or "}"

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

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

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

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v <= Hi} @-}

-- Error
{-@ adjustBound :: _ -> l:Nat -> {u:Nat | l <= u}  -> _ -> Btwn l (u+1) @-}
{-@ 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 さんありがとうございました。

以上です。

本記事で利用したコード