定理証明系 Haskellこの記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
