このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。
ちなみに 22 日目の担当者はそれぞれ
- Haskell Advent Calendar 2016 : heredocsの紹介 - Qiita
- Formal Method Advent Calendar 2016 : 農夫 山羊 キャベツ 狼 - Qiita
です。偶然ですが同じ方が執筆担当ですね。
さて、本エントリでは Haskell の型の表現力をより豊かにする仕組み、 LiquidHaskell について概要を紹介します。使用するサンプルコードは Samples of Verification by LiquidHaskell · GitHub にアップロードしてあります。
実行時エラーを防ぐには
簡単な例として、リストの先頭要素を取る関数 head の型を考えてみましょう。
*Main> :t head head :: [a] -> a
型としてはもちろんこれで正しいのですが、しかし空リストに対して haed を呼ぼうとすると実行時エラーが発生してしまいます。
*Main> head [] *** Exception: Prelude.head: empty list
では、このような実行時エラーをコンパイル時に、何らかの静的検査によって防ぐことはできないでしょうか？
head :: [a] -> a という型は、「何らかの型 a の要素を持つリストを引数に取って、同じ型 a を持つ値を返す」という head の制約を規定していますが、リストの長さについては何も主張していません。つまり上のエラーを防ぐためには、「引数となるリストが空でない」という事前条件を型にエンコードできればよいことになります。
これを実現する方法はいくつか考えられます。GADTs 言語拡張 を使って型レベル自然数を定義し、さらに型レベル自然数を長さとして持つ「長さ付きリスト型」を定義すれば空リストかどうかが型によって判定できそうです。また、依存型をフルに使える Haskell 以外の言語であればもっと素直な方法で表現できるでしょう。しかし、いずれも元の実装からは大きな改修が必要で、しかも関連箇所すべてを「長さ付きリスト型」で置き換えることになるため、なかなか骨が折れそうです。
LiquidHaskell では、専用のコメント {-@ ... @-} を使用して次のように記述します。
{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-} safeHead :: [a] -> a safeHead [] = liquidError "empty list" safeHead (x : _) = x
「長さが 0 を超える (= 空リストでない)」という事前条件がコメント内に型として表現されていることがわかります。LiquidHaskell が使用する情報は通常の GHC から見るとあくまでも単なるコメントであって、通常と同じように (検証を行わない) コンパイルが可能です。実際、ここでは分かりやすさ優先で safeHead と名前をつけましたが、関数名を head にしておけば呼び出し側モジュールの import 文を書き換えるだけで実装の差し替えが可能です。
新しく登場した liquidError が何者なのかは若干気になりますが、とりあえず先に処理系を動かせる状態を作りましょう。
インストールと最初の一歩
LiquidHaskell はバックエンドとして SMT ソルバを使用するため、あらかじめ本体とは別にセットアップしておく必要があります。自分の場合は Z3 の最新版 v4.5.0を選択しました。
本体の方は cabal でインストールするか、もしくはソースコードを clone してきて stack build でコンパイルするかの選択肢が提供されています。残念ながら Stackage には登録されていないようで、だいぶ前から "We are working to put liquid on stackage" のままになっています。
セットアップができたら先ほどの例を動かしてみましょう。以下のコードを Sample.hs として適当なところに保存し、liquid Sample.hs を実行してみてください。
module Sample where import Language.Haskell.Liquid.Prelude ( liquidError ) {-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-} safeHead [] = liquidError "empty list" safeHead (x : _) = x
実行時にいくつか進捗メッセージが表示されますが、最終的に
**** RESULT: SAFE **************************************************************
が表示されれば問題なくインストールできています。ようこそ、LiquidHaskell の世界へ！
LiquidHaskell の仕組み
型検査とサブタイピング
先ほどのコードスニペットをもう少しいじって動作を確かめてみましょう。まず、元のコードに次の関数を付け加えてみてください。
badUsage = safeHead []
safeHead を、事前条件に反して呼び出そうとしているわけです。liquid Sample.hs を実行すると、以下のようなエラーメッセージが返ってくるはずです。
**** RESULT: UNSAFE ************************************************************
/your/path/to/Sample.hs:9:12-22: Error: Liquid Type Mismatch
9 | badUsage = safeHead []
^^^^^^^^^^^
Inferred type
VV : {VV : [a] | len VV == 0
&& (null VV <=> true)
&& len VV >= 0
&& VV == ?a
&& len VV >= 0}
not a subtype of Required type
VV : {VV : [a] | len VV > 0}
In Context
?a : {?a : [a] | len ?a == 0
&& (null ?a <=> true)
&& len ?a >= 0}
「推論された型が要求された型のサブタイプではない」と言われていますね。
先ほど「a を要素とする空でないリスト」の型を { xs:[a] | len xs > 0 } と表現しましたが、LiquidHaskell では一般に「型 a のうち述語 P を満たすもの」は { x:a | P x } で表現されます。そして a 型の任意の値 x について P x => Q x が成り立つと SMT ソルバが判定した場合、LiquidHaskel は { x:a | P x} は { x:a | Q x } のサブタイプであると判断します。
この例でいえば、実引数 [] から推論された述語 len VV == 0 && ... から safeHead の事前条件 len VV > 0 は (当然) 従わないため、コンパイルエラーとして検出されているのです。
それでは逆に badUsage を削除、さらに safeHead の {-@ ... @-} コメントも無効化して実行してみましょう。今度は別のエラーになります。
**** RESULT: UNSAFE ************************************************************
/your/path/to/Sample.hs:6:32-43: Error: Liquid Type Mismatch
6 | safeHead [] = liquidError "empty list"
^^^^^^^^^^^^
Inferred type
VV : {VV : [Char] | VV ~~ ?b
&& len VV == strLen ?b
&& len VV >= 0
&& VV == ?a
&& len VV >= 0}
not a subtype of Required type
VV : {VV : [Char] | false}
In Context
?b : {?b : Addr# | ?b == "empty list"}
?a : {?a : [Char] | ?a ~~ ?b
&& len ?a == strLen ?b
&& len ?a >= 0}
これを見ると、liquidError の正体がわかります。
liquidError の引数として要求されている型は {VV : [Char] | false} です。false は決して真になることがない述語なので、いかなる引数であっても事前条件を満たすことができません。すなわち、liquidError は呼び出されうる場所に配置されると直ちにコンパイルを失敗させます。
もともとは safeHead の事前条件 { xs:[a] | len xs > 0 } が約束されていたためこのパターンマッチを通過しないことが LiquidHaskell によって推論されていたのですが、事前条件を外したことでエラーになったのでした。
もう少し単純な例を使って制約のかけ方を定式化してみましょう。
事前条件
上でも使用していたパターンですが、引数 (のうちのいくつか) に制約をつけることで関数の事前条件を表現することができます。例えば以下はゼロ除算エラーが発生しない割り算の定義です。
{-@ safeDiv :: Int -> { d:Int | d /= 0 } -> Int @-} safeDiv :: Int -> Int -> Int safeDiv n 0 = liquidError "zero divide" safeDiv n d = n `div` d
事前条件が指定されると、その関数のすべての呼び出しについて事前条件が守られているかどうかが検査されます。また、関数内のロジックや事後条件の検証は事前条件の仮定下で行われます。
事後条件
引数ではなく戻り値側に制約をつけて事後条件を表現することもできます。例えば以下は絶対値関数が常に 0 以上の値を返すことを表しています。
{-@ safeAbs :: Int -> { n:Int | n >= 0} @-} safeAbs :: Int -> Int safeAbs n | n >= 0 = n | otherwise = 0 - n
事後条件が指定されると、関数の事前条件および関数内のロジックから事後条件が従うかどうかが検査されます。また、他の関数内で呼び出された呼び出し側の検証は事後条件の仮定下で行われます。
事前条件に依存した事後条件
場合によっては、事前条件に依存した事後条件を記述する必要があります。
例えば整数に 1 を加算する関数について、事後条件に「戻り値は引数より真に大きい」という事後条件を与えてみましょう。条件を記述する際、次のように引数に名前をつけることができます。
{-@ safeIncr :: n:Int -> { v:Int | v > n } @-} safeIncr :: Int -> Int safeIncr n = n + 1
引数に事前条件を課し、さらに名前をつけて事後条件で引用することも可能です。
{-@ safeDouble :: n:{ v:Int | v > 2 } -> { w:Int | w > n + 2 } @-} safeDouble :: Int -> Int safeDouble n = 2 * n
例：ベクトルの次元付き計算
それでは例として、依存型を説明する際によく登場するベクトルの次元付き計算について、LiquidHaskell で表現してみましょう。
Haskell 上でベクトルを表現するもっともナイーブな方法は、単に Num インスタンスを要素とするリストを使用することです。例えばベクトル同士の足し算であればこんな感じでしょうか。
vecSum :: (Num a) => [a] -> [a] -> [a] vecSum xs ys = zipWith (+) xs ys
しかしお気付きの通り、次元が違うベクトル同士が加算できてしまうため、本来表現したい制約が表現できていません。
badSum = vecSum [1, 2, 3] [4, 5] *Main> badSum [5,7]
LiquidHaskell を使って、次元が異なるベクトルについて計算できないようにしてみましょう。そもそもの原因は、zipWith 関数が短い方のリストに合わせて残りを切り捨ててしまうことにあるため、まずこれを LiquidHaskell で書き直しておきます。
{-@ vecZipWith :: (a -> b -> c) -> xs:[a] -> { ys:[b] | len ys = len xs } -> { zs:[c] | len zs = len xs } @-} vecZipWith _ [] [] = [] vecZipWith f (x : xs) (y : ys) = f x y : vecZipWith f xs ys vecZipWith _ _ _ = liquidError "dimension mismatch"
事前条件として「第 2 引数の長さが第 1 引数に等しい」こと、さらに事後条件として「戻り値の長さが第 1 引数に等しいこと」が要求されています。この「次元付き zipWith」を使ってベクトルの足し算を以下のように定義すると
{-@ vecSum :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-} vecSum xs ys = vecZipWith (+) xs ys
LiquidHaskell は狙い通り警告を出してコンパイルを失敗させます。
/your/path/to/Sample.hs:37:10-33: Error: Liquid Type Mismatch
37 | badSum = vecSum [1, 2, 3] [4, 5]
^^^^^^^^^^^^^^^^^^^^^^^^
同様にして引き算や
{-@ vecSubtr :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-} vecSubtr xs ys = vecZipWith (-) xs ys
ベクトル同士の内積
{-@ dot :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> a @-} dot xs ys = sum $ vecZipWith (*) xs ys
あるいはベクトルのスカラー倍
{-@ vecMap :: (a -> b) -> xs:[a] -> { ys:[b] | len ys = len xs } @-} vecMap f [] = [] vecMap f (x : xs) = f x : vecMap f xs {-@ scalar :: (Num a) => a -> xs:[a] -> { ys:[a] | len ys = len xs } @-} scalar c xs = vecMap (c *) xs
も次元に対して安全に定義可能です。長さが正しくないリストをこれらの関数に与えて、実際にエラーになることを確認してみましょう。
まとめ
本エントリでは、LiquidHaskell を利用してリスト操作関数に対して事前条件と事後条件を定義する方法を扱いました。通常の Haskell ではリストの長さに関するエラーは型検査の対象外であり実行してみるまでわかりませんが、LiquidHaskell を用いることでコンパイル時に検出することができます。
今回紹介したのは、LiquidHaskell が持つ機能の一部分にすぎません。もし面白そうだと感じた人は、対話型チュートリアル もしくは 公式ブログ を眺めてみると良いと思います。というかこれを書いている自分自身もまだ全容を把握できていません。一緒に勉強しましょう。
さて、Advent Calendar の 24 日目の担当者はそれぞれ
- Haskell Advent Calendar 2016 : タイトル未定 (@maoe さん)
- Formal Method Advent Calendar 2016 : 空席
となっておりますが、それはまた別の話。
