関数型プログラミング入門 4 （型付ラムダ計算編）

本記事で学べること

・型付ラムダ計算

はじめに

関数型プログラミング入門 3 でラムダ計算の学習を終え、型付ラムダ計算について学ぶ準備ができたと思います。それでは早速、型付ラムダ計算について説明していきましょう。

(ラムダ計算に関してはこちらをチェック↓)

関数型プログラミング入門 3（ラムダ計算編）

型付ラムダ計算

型付ラムダ計算とは、ラムダ項に型をつけた形で計算を行うことをいいます。型は、基本型か、型 A, B を用いて A → B の形をした関数の型に分けられ、基本型には、例えば、整数の型 i や真偽値の型 o などが用いられます。
各変数にはその型が定まっているとします。例えば、変数 z の型は o で、変数 f の型は i → i という感じです。もし、変数 f の型が i → i で変数 a の型が i だった場合、fa の型は i になります。
ここで、ラムダ項は変数をもとに抽象と適用によって作られることを思い出しましょう。したがって、抽象と適用に対して型を定める規則を用意すれば、各々のラムダ項に型を定めることができます。λa.M という抽象は、a の型が A で M の型が B であれば、A → B というように定まります。また、MN という適用は、M の型が A → B で N の型が A であれば、B という型が定まります。
適用 MN に関しては、M の型が A → B という形をしていないか、もししていても N の型が A でない場合は型が定まらず、間違ったラムダ項になります。

型と簡約

ラムダ計算編のところで、β 簡約について学びました。ここで問題なのが、 β 簡約をしても型が保存されるのか、ということです。例えば、x, y, w の型を i として、(λx.λy.x)w というラムダ項を考えてみましょう。このとき、λx.λy.x の型は i → i → i で、w の型は i であるので、適用によって、(λx.λy.x)w の型は i → i となります。一方、(λx.λy.x)w を β 簡約した形が λy.w となります。このラムダ項の型も、同様に、i → i となり、 β 簡約前の型と一致します。一般に、ラムダ項の型は、β 簡約後も保存されます。これは、先の節で紹介した抽象と適用に対して型を定める規則が上手くできているためです。
余談ですが、正規化定理によって、β 簡約の停止性が証明されています。つまり、β 簡約は必ず有限ステップで停止します。

まとめ

本記事では型付ラムダ計算について解説をしました。ぜひ、本記事の内容をもとにして、より良い関数型プログラムを書いて欲しいところです。また、型付ラムダ計算には、証明とプログラムを対応づけるカリー・ハワード対応という非常に面白い考え方があります。これは、プログラムの高品質化に関わっている、最近ホットな話題といえます。こちらも機会があれば紹介したいと思います。では、さようなら〜。