開発部のxgotoです。Haskellの初級・中級者向けのトピックを取り上げたいと思います。
今回は型(Type)についてです。型はHaskellの入門書でも必ず最初のほうに説明されるもので、手元の本によれば、
型とは、互いに関連する値の集合である。
---- 『プログラミングHaskell』 Graham Hutton 著 / 山本和彦 訳
だとか、
値の世界は型と呼ばれる系統的な集まりへと分割される。
---- 『関数プログラミング入門 Haskellで学ぶ原理と技法』 Richard Bird 著 / 山下伸夫 訳
などのように書かれています。たとえば Bool は True と False の2つの値からなる集合だし、Intは整数の集合というように、型は値の集合というふうにみることができます。それならば型などと呼ばずに集合と呼べばいいと思いますが、「異なるものには異なる名前をつけろ」という先人の教えを信じれば、型というのは集合とは似て非なるものということになります。
型とは何か
では型は何者なのかというと、それは個々の型理論によるので一概になんだというのは難しいものです。たとえばマーティン・レフの型理論では型はSetoidのようなものと解釈されるし、ホモトピー型理論では空間として解釈されるし、Cubical型理論では立方体集合の何かで解釈されるし、という具合で、型理論では型が単なる集合として扱われることはまずありません。
そんな深遠で小難しい型ですが、プログラミングをする上で式や値の型を考えるというは極めて自然なことでもあります。たとえばシェルスクリプトでは明示的に型を書くことはありませんが、値がただの文字列 String なのか、それとも文字列のリスト [String] なのか、プログラマーは必ず頭の中で区別しているはずです。たとえ動的型付け言語であったとしても、ここはスカラコンテキストだとか、この変数の中身は数値だとか、意識しているはずです。
ド・ブラウン(De Bruijn)は、数学において（型なし集合論であるZF公理系などと比較して）型付き集合を採用することを熱く主張していました。彼の言葉を引用すれば、
I believe that thinking in terms of types and typed sets is much more natural than appealing to untyped set theory. Here the word natural of course refers to our mathematical culture and not to the nature of things or to the nature of mathematics.
型と型付き集合の観点から考えることは、型なし集合の理論に訴えるよりもはるかに自然だと思います。 ここで言う「自然な」という言葉は、もちろん私たちの数学的文化を指し、物事の性質や数学の性質を指すものではありません。（Google翻訳）
---- 『On the roles of types in mathematics』 N.G De Bruijn
拡大解釈かもしれませんが、同じことはプログラミングにも当てはまるのではないかと個人的には思っています。ド・ブラウンの熱い語りが個人的に大好きなのでもう少し引用しますが、
If we have a rational number and a set of points in the Euclidean plane, we cannot even imagine what it means to form the intersection. The idea that both might have been coded in ZF with a coding so crazy that the intersection is not empty seems to be ridiculous. (中略) Some types might be considered as subtypes of some other types, but in other cases two different types have nothing to do with each other. That does not mean that their intersection is empty, but that it would be insane to even talk about the intersection.
有理数とユークリッド平面上の点の集合があるとして、それらの交点を形成する意味をイメージすることはできません。 両方をZF公理系にクレイジーに符号化すれば交点が空ではないとみなせるかもしれない、という考えはばかげています。 （中略）一部の型は他の型の部分型と見なされる場合もありますが、そうでない場合は2つの異なる型は互いに関係ありません。それは交点が空であると言っているのではなく、交点について話すことさえ正気ではないということです。
---- 『On the roles of types in mathematics』 N.G De Bruijn
世の中には動的に型変換してよくわからない意味論の演算子をひたすら発明しているプログラミング言語もあるようですが、そのようなことはばかげているのであって、そのような演算子は便利でないと言っているのではなく、そのような演算子について話すことさえ正気ではない、ということです。（と私は感じました。）
型としての命題
そんな型ですが、Haskellerであれば（いやそうでなくても）ぜひ知っておきたいことがあります。それは俗に、型としての命題(Propositions as Types)と呼ばれるものです。これはカリー＝ハワード同型対応(Curry-Howard correspondence)とも呼ばれます。（このカリーとはハスケル・カリー(Haskell Brooks Curry)のことで、プログラミング言語Haskellの名前の元になった人でもあります）。
1934年、カリーはA -> Bという関数の型が「AならばB」という命題として読み替えることができるという興味深い事実を発見しました。さらにA -> B型の式（つまり関数）がこの命題の証明と対応することにも気づきました。その後の1969年、ハワードはカリーの考察をさらに推し進めて、同じ対応が自然演繹と単純型付ラムダ計算にも成り立つことをみつけ、さらにこの対応が表面上のものではなく、もっと深く対応していることを指摘しました。つまり式の評価が証明の簡約に対応していたわけです。（詳しい歴史については Propositions as Types - Philip Wadlerを参照してください。）
このPropositions as Typesという標語は、単に型が命題とみなせるというだけでなく、その型の式は命題の証明とみなせる(proofs as programs)というより深い対応があり、さらに式の評価はちゃんと証明の簡約に対応している(simplification of proofs as evaluation of programs)という、最深部まできっちりと対応しているということを言います。これは恐ろしい事実で、とても偶然一致したなどという話ではありえません。
とはいえ、こんな難しい話を聞いてもピンとこないので、実際に簡単な命題論理をHaskellで証明してみましょう。Propositions as Typesでは、命題を型であらわし、その型の関数を実装することで命題を証明する、という風に考えます。
まずは命題論理の基本的な推論規則であるモーダスポネンスを証明します。モーダスポネンスとは、「AならばB」と「A」が成り立つならば「B」も成り立つ、というものです。これをHaskellの型で表せば、
modus_ponens :: (a -> b) -> a -> b
という風になります（Haskellでは型変数は小文字なのでaやbを使いました）。これを実装するのは簡単で、
modus_ponens :: (a -> b) -> a -> b modus_ponens f a = f a
となります。これは簡単というよりも、むしろこれ以外の実装方法でまともなものはひとつもありません。（ほかの実装がありうるか考えてみてください、実はほかの実装がいくつかありえます… しかし今はそのことを忘れておきます）。
これは注意すべき事柄で、つまりあなたはこの型(a -> b) -> a -> bをみただけで、実際の実装をみなくても、その実装がほぼ完全に分かったはずだということです。もし関数を実装することが命題を証明することならば、当然めちゃくちゃな実装が許されるはずがありません。逆にもし実装できたのであれば、あなたはHaskellによる証明のチェックを通過したのであり、その実装はほぼ間違っているはずがない、ということでもあります。もちろん、これは極端な例ではありますが。
おれは仕様書を書かない、なぜならHaskellの型が仕様書だからだ！と豪語してまわりの反感を大人買いしているHaskellerがいるかもしれませんが、彼/彼女のいうことにも真理があったわけです。
次は三段論法を証明してみましょう。三段論法とは、よく知っているとは思いますが、「AならばB」と「BならばC」が成り立つならば「AならばC」が成り立つ、というものです。これをHaskellの型で表すと、
syllogism :: (a -> b) -> (b -> c) -> (a -> c)
となります。これもまともな実装は一通りしかなく、
syllogism :: (a -> b) -> (b -> c) -> (a -> c) syllogism f g = g . f
となります。
さて命題論理では命題の否定￢があります。これはどのように型で表せれるのでしょうか？単純には表現しづらいですが、少し見方を変えるとできます。「Aでない(￢A)」というのは、もしAが証明できてしまったら矛盾している、という風に考えることができます。では矛盾している命題、つまり証明できていはいけない命題は型で表現できるのでしょうか？
証明＝実装なので、証明できてはいけないのならば、絶対に実装できない型でなければいけません。Haskellでは空のデータ型を使うことができます。
data Bottom
この界隈では矛盾のことをよくボトム(Bottom, ⊥)と呼びます。名前はさておき、このBottom型は、普通ならあるはずのデータ型宣言の右側がありません。つまりデータコンストラクタがないため、このBottom型の値を作成することはできません。よってこれが矛盾を表す型として使えます。
そして「Aでない(￢A)」というのは、Bottomを使ってA -> Bottomという型で表すことができます。もしAの値が手に入ると、この型の関数を使ってBottomを作れてしまい矛盾します。つまりAの値は手に入らない、ということを表しています。
命題の否定が手に入ったので、さっそく対偶が成り立つか確認してみましょう。対偶とは「AならばB」ならば「￢Bならば￢A」というものでした。これをHaskellの型で書くと、
contra :: (a -> b) -> (b -> Bottom) -> (a -> Bottom)
となります。少しややこしい型になりましたが、これも以下のように実装することができます。
contra :: (a -> b) -> (b -> Bottom) -> (a -> Bottom) contra f notb a = notb (f a)
この a -> Bottom は頻繁に使いますが、型としては少し読みづらいので型シノニムを使って別名をつけておきます。
type Not a = a -> Bottom
これを使うと先ほどのcontraの型は以下のようになります。
contra :: (a -> b) -> Not b -> Not a
論理パズルに挑戦
ここまでで大分こつが掴めてきたと思います。せっかくなのでもう少し面白いものを解いてみましょう。
『不思議の国のアリス』で有名なルイス・キャロル(Lewis Carroll)は、実際にはオックスフォード大学の数学の教授だったそうです。彼が論理とナンセンスが大好きだっただろうことは本からよくわかりますが、彼は一般人向けに論理的な思考の訓練のためのパズルを作成していたそうです。ということで、このWebサイト(3E Lewis Carroll Puzzles)からキャロルの問題をいくつか引用します。
- （a）すべての赤ちゃんは非論理的です
- （b）クロコダイルを手なずけられる人は嫌われません
- （c）非論理的な人は嫌われています
さてこの３つ文から導けることは何でしょうか？赤ちゃんはクロコダイルを手なずけられるでしょうか？答えは、手なずけられない、です。それをHaskellで導いてみましょう。
まず文章を命題論理として扱うために、すべてを記号に置きかえます：
B : 赤ちゃんである L : 論理的である M : クロコダイルを手なずけられる D : 嫌われている
このように記号を置けば、上の３つの文章は次のように言い換えることができます：
- (a)
B -> Not L - (b)
M -> Not D - (c)
Not L -> D
この３つを前提として、導きたい答えは「赤ちゃんはクロコダイルを手なずけられない B -> Not M」です。これをHaskellの型であらわすと、
puzzle :: (b -> Not l) -> (m -> Not d) -> (Not l -> d) -> (b -> Not m)
となります。かつてない長さの型ですね。実装は思ったよりもストレートです：
puzzle :: (b -> Not l) -> (m -> Not d) -> (Not l -> d) -> (b -> Not m) puzzle b_notl m_notd notl_d b m = m_notd m (notl_d (b_notl b))
排中律の悪魔
命題論理では「AならばB」のような含意のほかに、「AかつB」や「AまたはB」なども記述できます。これらもHaskellの型で表現することができて、それぞれ、「AかつB(a, b)」、「AまたはBEither a b」と書けます。以上を組み合わせることで表現できる論理は直観論理(intuitionistic logic)と呼ばれます。
今まで見てきたように、直観論理における証明は、具体的な式を実際に構成してみせることで行います。この構成的な性格のため、直観論理では古典論理で成り立ついくつかの命題が成り立ちません。たとえば二重否定の除去(￢￢AならばA)や排中律（Aまたは￢A)を直観論理で証明することはできません：
-- 二重否定の除去 double_negative_elim :: Not (Not a) -> a -- 排中律 excluded_middle :: Either a (Not a)
だとすると、直観論理はなにか不整合があるのかと思われるかもしれませんが、そういうわけではありません。直観論理においては、排中律は肯定することも否定することもできないので、独立した公理としてみなされます。つまり、もし排中律を公理として直観論理に足したとしてもなにも矛盾は起きません。そういう意味で、直観論理は古典論理よりも一般的で豊かな論理であるとみることができます。
「直観論理では排中律を肯定することも否定することもできない」と書きましたが、この証明はちょっと興味深いものなので、ここで紹介します。排中律を肯定することができないというのは、なんとなく分かりますが、否定することができないとはどういうことでしょうか？
実は直観論理では排中律の否定を否定的に証明できます。これは相当むずかしいので、論理パズルが簡単すぎた方はぜひ挑戦してみてください（証明の答えは、このずっと下に出てきます）。
lem_irrefutable :: Not (Not (Either a (Not a)))
二重否定の除去(￢￢AならばA)は直観論理にはないことに注意してください。この関数はその実装の形から、排中律の悪魔(the devil of the excluded middle)と呼ばれることもあります(Call-by-Value is Dual to Call-by-Name)。この悪魔には面白い寓話があるので、最後にそれを紹介します。
昔々、悪魔が男のもとにきて言った。
「(a) 君に10億ドルあげるか、(b) もし君が10億ドルくれたらどんな願いでも叶えてあげよう。ただし、(a)か(b)のどちらを提示するかはおれが決める」
男は用心深く、魂を明け渡す必要があるか確認した。「いいや、君がする必要があるのは申し出を受け入れることだけだ」と悪魔は答えた。
男は考えた。もし(b)を提示された場合、願いを買うことはとてもできないが、しかしこのチャンスを利用したところで何か害があるわけでもない。結局、男は「受け入れます」と答えた。「それで(a)なのか？(b)なのか？」
悪魔は少し考えて「(b)だな」と答えた。
男は失望したが、驚くことはなかった。それはそうだと思った。しかしどんな願いでも叶えられるという申し出は男を蝕んだ。それから男は何年もお金を貯め始めた。時には悪いこともした。そしてそれこそが悪魔の狙いだったんだろうとぼんやりと思った。やがて男は10億ドルを手にし、そして悪魔が再び男の前に現れた。
「ここに10億ドルある」そう言って男はお金を手渡した。「願いを叶えてくれ！」
悪魔はお金を手に取り、男に言った、「あれ、おれは前に(b)なんて言ったっけ？ごめん、(a)のつもりだったんだ。君に10億ドルあげれてとても嬉しいよ」そういって悪魔は、今受け取ったお金をそのまま男へ返した。
---- Call-by-Value is Dual to Call-by-Name, Philip Wadler
この話だけ読んでも意味不明ですが、排中律の否定の否定の実装と見比べると意味がわかります。ということで、先ほどの答えを書きますと、
lem_irrefutable :: Not (Not (Either a (Not a))) lem_irrefutable choose = choose (Right (\money -> choose (Left money)))
となります。話に合わせて変数名をchooseとmoneyにしてみました。このchooseはいわゆる継続(continuation)になっており、悪魔はまず最初に男にRightつまり(b)を渡しておき、そのあとでもし男が10億ドルのお金を持って戻ってきたら、ただちにLeftつまり(a)に切り替えて継続を呼びなおす、というとても悪魔らしいずるいことをやります。この式を計算的に実行するとそのように解釈できる、という話でした。
いかがでしたでしょうか。少しでもHaskellと型に興味を持ってもらえたら幸いです。
採用情報
朝日ネットでは新卒採用・キャリア採用を行っております。
