ITpro連載第14回型＝命題，プログラム＝証明

ややブームに乗り遅れた(?)感もありますが、カリー・ハワード同型（のさわり）の話です。

追記：直観主義論理＋二重否定の除去（¬¬Ａ⇒Ａ）だけから排中律（Ａ∨¬Ａ）を示す、などに興味のある方もどうぞ（¬Ａの定義はＡ⇒False）。

追記２：ぎく(2007-9-17)。「MLでは」なのと、「再帰(rec)や組み込み関数を使わずに」が前提ということで…（OCaml onlyだと、それこそObj.magic 0 : 'aとかあるので）

追記３：ちなみに上のリンク先のリンク先によれば、「type void」はバリアント型の定義ではなく抽象データ型の宣言だそうなので、GHCの「data Void」とは少し違う…？