すべてのものは…である
SmalltalkやRubyなど,いわゆる生粋のオブジェクト指向言語では,「すべてのものはオブジェクトである」(everything is an object)と言われることがある。JavaやC++などと異なり,整数の「123」や浮動小数の「4.56」といった,基本データ型の値もオブジェクトとして扱うことができるからだ(ちなみに,現在のJavaには自動ボックス化という機能があり,基本データ型からオブジェクト型への変換が自動で行われる場合も多い。しかし,両者の差異が全くなくなったわけではない。例えば123.toString()のようなメソッド呼び出しはできない)。
では,オブジェクト指向言語のまねをして,関数型言語において「すべてのものは関数である」と言うことはできるだろうか?
もちろん,オブジェクト指向と違って,関数型プログラミングはあくまで「数学的な(=副作用のない)関数を中心とするプログラミング」に過ぎず,「すべてのものを関数とみなす」ことを目指しているわけではない。したがって,通常,「123」や「4.56」を関数とみなす,といった欲求はない。
ところが,関数型言語のモデルとなっている基礎理論では,実は「すべてのものを関数で表す」ことができる。より正確にいうと,(計算機自体の一般的なモデルである)「チューリングマシン」で可能な計算は,すべて関数で表せることが知られている。それが今回紹介するλ計算(ラムダ計算)という計算モデルだ。
λ計算の構文と直観的意味
本連載第11回で紹介した,並行言語のモデルであるπ計算と同様(あるいはそれ以上)に,λ計算にも非常に様々な変種がある。
今回は,それらすべての基本となる,もっとも純粋なλ計算について紹介しよう(なお,ここでいう「純粋」は,「副作用がない」という意味の「純粋」とは関係がない。整数などを関数で表すのではなく,プリミティブとして追加した「応用λ計算」も存在する。第10回でインタプリタを作成したMyFun言語も,応用λ計算の一種だ)。
純粋なλ計算は,一言でいうと「関数しかないプログラミング言語」だ。純粋なλ計算のプログラム(λ式)の構文は,以下の3行で表される。
- λ抽象「λx. e」
- 関数適用「e1 e2」
- 変数「x」
ただし,xは変数一般を表す記号,e,e1,e2などはλ式一般を表す記号とする。
λ抽象「λx. e」は,OCamlの「fun x -> e」に相当する構文で,xを受け取ると,eを評価して返す関数を表す。関数適用と変数の意味はOCamlと同様だ。
論理値と条件式をλ式で表す
たったこれだけの構文で,関数型言語の様々な式や値をどうやって表現するのだろうか?
まず,簡単な例として,変数を定義するlet式「let x = e1 in e2」を考えてみよう。これは(λx. e2) e1というλ式で表すことができる。どちらも,まず変数xがe1(ないしe1を評価して得られる値)に束縛され,それからe2が評価されるからだ。
では,条件式「if e1 then e2 else e3」はどうだろうか。この式は,e1がtrueになればe2に,e1がfalseになればe3になってほしいはずだ。そのためには,まず,trueやfalseをどう表すかを考えなければならない。
ここで,ちょっと発想を逆転して,trueやfalse自身にif式の動作を「仕込む」ことにしよう。つまり,「e2とe3を受け取って,e2のほうを返す」関数でtrueを,e3のほうを返す関数でfalseを表すことにする。
true = λx. λy. x false = λx. λy. y
trueやfalse自身に条件分岐の機能を「仕込んだ」ので,if式はe1にe2とe3を与えるだけで良い。
if e1 then e2 else e3 = e1 e2 e3
そうすれば,確かにif true then e2 else e3は,(λx. λy. x) e2 e3つまりe2となる。同様にif false then e2 else e3はe3となる。true,falseとif式が表せれば,&&や||といった論理演算も容易に表現できる。
e1 && e2 = if e1 then e2 else false e1 || e2 = if e1 then true else e2 not(e) = if e then false else true
ただし,OCamlのような値呼び(call-by-value)の言語では,関数適用の前に引数が評価されるので,「e1 e2 e3」ではe2やe3が先に評価されてしまう。つまり,if式のthen節とelse節が両方とも評価されてしまう。
仮に入出力や例外などの副作用はないとしても,e2やe3が無限ループすることはあり得るので,これはまずい。λ計算自身は一般的なモデルなので,値呼び以外の評価順を考えることもできるが,値呼びも考慮したい場合は,以下のようにe2やe3をダミーの引数を受け取る関数とすれば良い。
if e1 then e2 else e3 = e1 (λd. e2) (λd. e3) true = λx. λy. x e false = λx. λy. y e
ただし,dはe2やe3に出現しない変数で,eは適当なダミーのλ式(例えばλx. xなど)とする。
試しに,true && falseに当たるλ式がどのような値に評価されるか,OCamlで確認してみよう。まず,OCamlのプリミティブ値である「true」や「false」とは別に,上のように関数で表した「my_true」と「my_false」を定義する。また,型をわかりやすく表示するために,'a my_bool型も定義する。'a my_boolの'aは,その論理値に対する条件分岐の結果の型に当たる。一つの論理値をいろいろな型のif式で使うために,'aという型変数にしておくわけだ。また,上のダミー変数dやダミー式eの型として,'a my_unit型も定義する。
# type 'a my_unit = 'a -> 'a ;; type 'a my_unit = 'a -> 'a # type 'a my_bool = ('a my_unit -> 'a) -> ('a my_unit -> 'a) -> 'a ;; type 'a my_bool = ('a my_unit -> 'a) -> ('a my_unit -> 'a) -> 'a # let e : 'a my_unit = fun x -> x ;; val e : 'a my_unit = <fun> # let my_true : 'a my_bool = fun x -> fun y -> x e ;; val my_true : 'a my_bool = <fun> # let my_false : 'a my_bool = fun x -> fun y -> y e ;; val my_false : 'a my_bool = <fun>
先の考え方に従えば,true && falseはif true then false else falseつまりtrue (λd. false) (λd. false)と表せるはずだ。
# let ans1 : 'a my_bool = my_true (fun d -> my_false) (fun d -> my_false) ;; val ans1 : '_a my_bool = <fun>
しかし,このままでは,答えであるはずの関数ans1が単に<fun>と表示されてしまい,中身を確かめることができない。そこで,前回のtype-directed部分評価を使って,ans1の無駄な部分を省略した「ソースコード」を復元してみよう。型がややこしいが,ここでは深く考えないことにして,前回と同様,型変数は「z」で,->は^->で機械的に置き換えれば良い(ただし,前回は関数適用の前後の括弧を省略してしまったので,"%s %s"を"(%s %s)" に修正しておく必要がある)。
# val2str (((z ^-> z) ^-> z) ^-> ((z ^-> z) ^-> z) ^-> z) ans1 ;; - : string = "(fun x1 -> (fun x2 -> (x2 (fun x3 -> x3))))"
これは確かに上のmy_falseと(引数の名前や括弧など以外は)「同じ」式になっている。