NGK2017B で Liquid Haskell について話してきました

先日、毎年恒例のなごや LT 大会 NGK2017B / 名古屋合同懇親会 2017 忘年会で発表してきました。

Liquid Haskell で普通の型システムの上を行け #NGK2017B from y_taka_23

www.slideshare.net

当日の動画は NGK2017B 第2部 - YouTube から見ることができます。

ちなみに NGK での発表は 5 年連続 5 回目です。前回まではモデル検査をテーマにしていましたが、今回はちょっと目先を変えて（とはいえ同じ形式手法の枠内ですが）もう少しプログラム寄りの題材として Liquid Haskell を選びました。

NGK2013B : Alloy ではじめる簡単モデル検査
NGK2014B : 猫でもわかる！モデル検査器 SPIN 入門（ブログ記事）
NGK2015B : AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計（ブログ記事）
NGK2016B : 机上の Kubernetes - 形式手法で見るコンテナオーケストレーション #NGK2016B（ブログ記事）

発表中のサンプルについて

今回の発表では、Heartbleed 脆弱性を模した次のようなコードをサンプルとして取り上げました。

module Main where

import Data.Text
import Data.Text.Unsafe

{-@ measure tlen :: Text -> Int                                     @-}
{-@ assume  pack :: s:String -> { t:Text | tlen t == len s }        @-}
{-@ assume  takeWord16 :: n:Int -> { t:Text | tlen t >= n } -> Text @-}

output :: Text
output = takeWord16 10 (pack "input")

このアイデアは、 ICFP 2016 で行われた Niki Vazou さんのチュートリアルから拝借させていただいたものです。

Programming with Refinement Types

上のコードからもわかる通り、takeWord16 は Data.Text.Unsafe モジュール内にあり、あくまでも unsafe な関数であることは明示されています。LT ではあえて「C 言語と同レベル」と煽ってみましたが、そもそも Haskell 本来の哲学からは外れた関数であることには留意してもらえると幸いです。

特に注目したいポイントは以下の 2 点です。

main 関数がない : エントリポイントがないため、プログラムは実行されておらずあくまでも静的な検証のみが行われていることがわかります。にもかかわらず、通常であれば実行時まで発見できないはずのロジックや値の範囲のエラーが検証できることこそが Liquid Haskell のメリットです。

篩型はコメントで記述する : 言語自体に特殊な追加要素を持ち込むことなく、コメントとして制約を記述します。通常の GHC から見ると{-@ ... @-} 内は単なるコメントでしかないため、Liquid Haskell を使用しない環境でもソースを変更することなくコンパイル可能です。

ちなみに、Liquid Haskell については去年の Advent Calendar でも解説しています。今回のスライドと合わせて読むと理解が深まるはずですが、それはまた別の話。

ccvanishing.hateblo.jp