関数を扱えることはどのようにプログラミング言語の能力をあげるか

Java8で関数が値として扱えるようになりました。
このことが、「関数が渡せると便利だよね」という観点ではなく、プログラミング言語としての能力をどのようにあげるか考えてみます。

圏論からのテクニックが使いやすくなる

集合論はどちらかというと値にたいする理論でしたが、圏論は関数呼び出しに関する理論です。
プログラムには、関数呼び出しを連結させて値を変換していくという側面があります。
そのような関数呼び出しの扱い方を整理するのが圏論で、圏論の考え方を使うことでより安定したプログラムを書くことができます。
モナドなど圏論由来のテクニックを使うには、どうしても関数を値として扱う必要があります。

関数を値として扱うことで、圏論のテクニックが使いやすくなり、安定したプログラムの書きやすさにつながります。

型の証明能力があがる

動的な型付の言語にくらべて、静的な型付の言語はプログラムが間違いにくいといわれます。
コンパイル時に検査ができるからなのですが、型の検査が通るということは、実は証明が行われたということになります。
カリー・ハワード同型対応といって、プログラムの型と、論理の証明は、同じものであることが示されています。
つまり、「Aという型である」ということは、「Aである」ということの証明です。
そして、「Aという引数をとってBを返す関数」を実装することは「AならばBである」ことの証明になります。

関数を値として扱うことでは、実際には証明能力は変わりませんが、命題の記述しやすさが変わり、コンパイルが通った時点で保証できる範囲が広げやすくなります。

型による証明

型による証明について補足しておきます。

たとえば

Flyable proof(Bird a)

という関数の実装は、「BirdならばFlyableである」ということの証明です。

引数をふたつとると、それは「かつ」になります。

Pettable proof(Bird a, Small s)

という関数の定義は「Birdであり、かつSmallならば、Pettableである」ということの証明です。
(Pettableという単語があるかどうかしりませんが、ここでは飼うことができる程度の意味だと思ってください)

関数が値として使えるようになると、「ならば」を前提条件に組み合わせることができます。
たとえば

Flyable proof(Bird a, Function f)

という関数の実装は「Birdであり、かつBirdならばFlyableであるならば、Flyableである」という証明になります。
この場合、「return f.apply(a)」とすればBirdやFlyableがどのようなものであるかにかかわらず常に実装可能です。つまり、これは恒真式であるということです。

三段論法の証明も可能です。

Function proof(Function fc, Function fb)

という関数の実装は、「CrowならばBird、かつBirdならばFlyableであれば、CrowならばFlyable」つまり「カラスが鳥であり、鳥が飛ぶならば、カラスは飛ぶ」という証明です。
この実装は

return (Crow c) -> fb.apply(fc.apply(c));

とすれば常に可能です。少々賢い推論エンジンがあれば、自動的にかけます。つまり自明ということです。
三段論法が証明できました！

つぎのような関数があるとします。

Function proof(Function ff, Function fb)

これは「CrowならばFlyable、かつCrowならばBlackであれば、BlackならばFlyable」つまり「カラスは飛び、カラスが黒いならば、黒いものは飛ぶ」という論理式に対応します。
しかしこれは、無条件では実装できません。自明ではないということです。
実装するとしたら、次のようになります。

return (Black b) -> { if (b instanceof Crow) return ff.apply((Crow)b) else throw new RuntimeException()}

黒いものがカラスの場合だけ飛ぶわけですね。また、Exceptionを投げる、つまり関数が終了しないということは、論理としては偽をあらわします。たぶん。

さまざまな証明を行おうとすると、Javaの型システムでは全く足りませんが、関数を扱うことで証明の能力があがることは確かです。

参考書籍

圏論をプログラムの文脈で説明している本には、「プログラム意味論」があります。「カテゴリー理論」というのが圏論です。しかし、そこにたどりつくまでが結構つらい。あと、モノイドの説明など、圏論の文脈としてはあまり厳密でない表現もある感じです。

プログラム意味論 (情報数学講座)

圏論がタイトルになっている本は、３冊ほどよく名前を目にしますが、竹内先生の本がいいようです。

層・圏・トポス―現代的集合像を求めて

「圏論による論理学」を持っていますが、論理学と対比しつつ進んでいるので、圏論だけを勉強しようとするとちょっと読みにくいです。

カリー・ハワード同型対応については、「論理と計算のしくみ」の最後に載っています。

論理と計算のしくみ

ただ、論理系の本では型と論理がどのように対応するかの説明であることに対して、この本では、カリー・ハワード同型対応がどのような価値があるか、どのような意味をもつかという解説がされていて、非常におすすめです。残念ながら絶版ですけど。

知の教科書　論理の哲学 (講談社選書メチエ)