コンパイルは(テストではなく)証明である

「プログラムのテストはバグの存在を示すことにかけてはとても効率的な方法ですが、バグの不在を示すことにかけては絶望的なほどに不適切です。プログラムの信頼性を顕著に向上させる唯一の方法は、その正当性に対して説得力のある証明を与えることです」 -- Edsger W. Dijkstra

静的型付き言語では、コンパイル時に型が検査される。この型検査に関連して型推論という機能を持つ言語がある。型推論は、大きく分けて2つの意味で使われているようだ。

命令型言語の多くに見られる型推論：型検査の過程で、省略された型を補うこと
関数型言語の多くに見られる型推論：未知の型を変数として方程式を立て、方程式を解いて未知の型を求めること。型推論自体が型検査の役割を果たす

この記事では、後者の型推論を話題にする。

静的型付き関数型言語の利点として、よく「コンパイルはテストである」という説明がなされる。プログラムは式で構成されており、あらゆる部分式が検査の対象となる。コーディング → コンパイルの繰り返しは、言わば最も安価なテスト駆動開発だ。

「コンパイルはテストである」という説明は、実は多くのプログラマに分かるように配慮された控えめな表現である。本当のことをいうと「コンパイルは証明」なのだ。

型推論を持つ静的型付き関数型でコードをコンパイルし、型推論による型検査をパスしたなら、型に関するバグは存在しないことが保証される。繰り返しになるが、そう、「コンパイルはテストではなく証明」なのだ。

コンパイルに通れば型に関するバグはないが、値に対するバグは存在しうるので、もちろんテストを疎かにしてはいけない。しかし、型推論による型検査がない言語に比べて、テストしなければならない項目は激減する。

型推論による型検査は、安価で便利な自動証明の仕組みだ。静的型付き関数型言語を好むプログラマは「こんなよいものを使わない手はない」と考えている。

型エラーを引き延ばす

しかし、初心者であれば型に関する間違いがあってもプログラムを動かしたいと思うだろう。その気持ちは、よく分かる。僕も昔はそうだったから。

静的型付き関数型言語の処理系によっては、コンパイル時の型エラーを実行時まで引き延ばす機能を提供する。たとえば、Haskell の処理系である GHC の最新版は、その機能を持つ。

以下のコードを考える：

module Main where

main :: IO ()
main = do
    -- putStrLn は文字列を取る
    putStrLn "Hello, world!" 
    putStrLn 1               -- 型エラー

単純にコンパイルしてみる。

% ghc Main.hs
[1 of 1] Compiling Main             ( Main.hs, Main.o )

Main.hs:7:14:
    No instance for (Num String) arising from the literal `1'
    Possible fix: add an instance declaration for (Num String)
    In the first argument of `putStrLn', namely `1'
    In a stmt of a 'do' block: putStrLn 1
    In the expression:
      do { putStrLn "Hello, world!";
           putStrLn 1 }

型エラーとなった。次に -fdefer-type-errors というオプションを指定してコンパイルしてみる。

% ghc -fdefer-type-errors Main.hs
[1 of 1] Compiling Main             ( Main.hs, Main.o )

Main.hs:7:14: Warning:
    No instance for (Num String) arising from the literal `1'
    Possible fix: add an instance declaration for (Num String)
    In the first argument of `putStrLn', namely `1'
    In a stmt of a 'do' block: putStrLn 1
    In the expression:
      do { putStrLn "Hello, world!";
           putStrLn 1 }
Linking Main ...

リンクまで到達することが分かる。実行してみよう。

~% ./Main
Hello, world!
Main: Main.hs:7:14:
    No instance for (Num String) arising from the literal `1'
    Possible fix: add an instance declaration for (Num String)
    In the first argument of `putStrLn', namely `1'
    In a stmt of a 'do' block: putStrLn 1
    In the expression:
      do { putStrLn "Hello, world!";
           putStrLn 1 }
(deferred type error)

"Hello, world!" を表示した後に型エラーになった。

その内「明らかに誤りのあるコードを動かして何が嬉しいのか」という考え方になるかもしれないが、それまでの間、この機能は便利かもしれない。

(追記) runghc にこのオプションを指定するには "--" が必要のようだ。