はじめに

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

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

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

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

LiquidHaskell とは?

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

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

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

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

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

インストール

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

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

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

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

SMT ソルバのインストール

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

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

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

Ubuntu 18.04

$ sudo apt update
$ sudo apt install z3

$ z3 --version
Z3 version 4.4.1

macOS Catalina 10.15.4

brew でインストールする場合は以下の通りです。

$ brew install z3

$ z3 --version
Z3 version 4.8.7 - 64 bit

LiquidHaskell のインストール

現状、一番安定しているのは hackageliquidhaskellcabalGHC-8.6.5 の組み合わせでインストールする方法だと思います。その他のインストール方法等は INSTALL.md をご参照下さい。

$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 8.6.5

$ cabal -V
cabal-install version 3.2.0.0
compiled using version 3.2.0.0 of the Cabal library
$ cabal update
$ cabal install liquidhaskell

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

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

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

Targets:

サンプルプログラム

シンプルな 0 除算の例を使って LiquidHaskell に慣れましょう!

-- MyDiv.hs
module MyDiv where

myDiv :: Int -> Int -> Int
myDiv = div

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

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

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

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

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

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

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

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

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

{-@ myDiv :: Int -> Int -> Int @-} -- これが篩型
myDiv :: Int -> Int -> Int
myDiv = div

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

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

MyDiv.hs:5:1-11: Error: Liquid Type Mismatch
  
 5 | myDiv = div
     ^^^^^^^^^^^
  
   Inferred type
     VV : GHC.Types.Int
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV /= 0}

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

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

{-@ div :: Int -> {v:Int | v /= 0} -> Int @-}

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

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

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

{-@ myDiv :: Int -> Int -> Int @-}
myDiv :: Int -> Int -> Int
myDiv = div

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

{-@ myDiv :: Int -> {v:Int | v /= 0} -> Int @-}
myDiv :: Int -> Int -> Int
myDiv = div

これで SAFE になります。

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

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

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

{-@ type NonZero = {v:Int | v /= 0} @-}

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

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ myDiv :: Int -> NonZero -> Int @-}
myDiv :: Int -> Int -> Int
myDiv = div

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

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

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

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

good :: Int
good = myDiv 10 2

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

bad :: Int
bad = myDiv 10 0
$ liquid MyDiv.hs
**** RESULT: UNSAFE ************************************************************

MyDiv.hs:12:16: Error: Liquid Type Mismatch
  
 12 | bad = myDiv 10 0
                     ^
  
   Inferred type
     VV : {v : GHC.Types.Int | v == 0}
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV /= 0}

問題

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

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

-- Main.hs
module Main where

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ myDiv :: Int -> NonZero -> Int @-}
myDiv :: Int -> Int -> Int
myDiv = div

{-@ lazy main @-}
main :: IO ()
main = do
  n <- getLine
  m <- getLine
  case safeDiv (read n) (read m) of
    Just res -> print res
    Nothing -> do
      putStrLn "第二引数に0が入力されています"
      putStrLn "もう一度入力してください"
      main

{-@ safeDiv :: Int -> Int -> Maybe Int @-}
safeDiv :: Int -> Int -> Maybe Int
safeDiv n m
  | check     = Just $ div n m
  | otherwise = Nothing
  where
   check = True

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

エラーメッセージ

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

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

Main.hs:24:30: Error: Liquid Type Mismatch
  
 24 |   | check     = Just $ div n m
                                   ^
  
   Inferred type
     VV : {v : GHC.Types.Int | v == m}
  
   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV /= 0}
  
   In Context
     m : GHC.Types.Int

実行例

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

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

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

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

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

興味を持った方へ

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

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

日本語の情報

ブログ

チュートリアル

スライド

  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 @-} で記述する

以上です。

本記事で利用したコード