前回,'a * 'b -> 'b * 'aといったMLの型は,「AかつBならばBかつA」といった命題に対応する,という話をした。命題が成り立つことは,そのような型を持つ式が存在することに対応するのだった(ただし例外などの副作用や無限ループ,組み込み関数やライブラリ関数などは使用しないとする。以下同様)。
前回の繰り返しになるが,'a * 'b -> 'b * 'aは,「任意の型'aと'bについて,'a型の値と'b型の値の組を受け取り,'b型の値と'a型の値の組を返す」という関数の型だ。そのような型を持つ式としては,例えば以下のような関数が存在した。
# fun (x, y) -> (y, x) ;; - : 'a * 'b -> 'b * 'a = <fun>
型から関数の中身を当てる
では,逆にfun (x, y) -> (y, x)以外に,'a * 'b -> 'b * 'aという型を持つ関数は存在するのだろうか?
もし,xやyを整数や浮動小数として演算に使用してしまうと,型が特定されてしまい,「任意の'aと'bについて…」という型にはならない。
# fun (x, y) -> (y + 1, x *. 2.3) ;; - : float * int -> int * float = <fun>
また,xやyを関数や組として使用した場合も,'a * 'b -> 'b * 'aより「複雑」な(より特定された)型になってしまう。例えば,下の例では,xの型が'a * 'bという組型に,yの型がunit -> 'cという関数型に特定されてしまう。
# fun (x, y) -> fst x; (* xを組とみなして,第一要素を取り出す *) y (); (* yを関数とみなして,unit型のダミー値()に適用する *) (y, x) ;; - : ('a * 'b) * (unit -> 'c) -> (unit -> 'c) * ('a * 'b) = <fun>
このように,xやyを実際に使用してしまうと,型が特定されてしまい,'a * 'b -> 'b * 'aとはならない。
では,以下のような関数はどうだろうか。
# fun (x, y) -> let z = (y, x) in (* yとxの組をzとおく *) (* zの第一要素と第二要素を取り出し,組を作り直す *) (fst z, snd z) ;; - : 'a * 'b -> 'b * 'a = <fun>
この例では,まずyとxの組を作ってから,それらの要素を取り出し,同じ組を作り直している。この関数は,確かに'a * 'b -> 'b * 'aという型を持つ。しかし,「要素を取り出し,同じ組を作り直す」という操作は明らかに無駄で,特に意味がない。言い換えると,実行速度やメモリー消費の問題を無視すれば,上の式はfun (x, y) -> (y, x)と全く等価な動作をする。
このように考えると,'a * 'b -> 'b * 'a という型を持つ関数は,fun (x, y) -> (y, x)と等価になることが知られている。
別の例として,'a -> 'aという型を考えてみよう。これは「すべての型'aについて,'a型の引数を受け取ると,'a型の結果を返す」という関数の型だ。そのような関数としては,受け取った値をそのまま返す恒等関数fun x -> xがある。逆に,'a -> 'a型の(副作用などのない)関数は,すべてfun x -> xと等価になることが知られている。
さらに別の例として,unit -> 'aという型を考えよう。前回の対応によれば,この型は「任意のAについて,trueならばA」という命題を表す。そのような命題が成立するわけはないので,unit -> 'a型の(副作用などのない)関数は存在しないといえる。
逆に言うと,unit -> 'a型の関数は決して正常に値を返さず,呼び出すと必ず無限ループや例外などを起こすことがわかる。「任意の型'aについて,ダミーの値( )を受け取って,'a型の値を返す」という動作は実現不能だからだ。そのような関数としては,前回も触れたが,例えば以下のような例がある。
# let rec f () = f () ;; val f : unit -> 'a = <fun> # fun () -> failwith "exception" ;; - : unit -> 'a = <fun>
型と値から関数の「ソースコード」を復元する
では,'a -> 'a -> 'aという型を持つ関数はどうだろうか。これは「すべての型'aについて,'a型の引数を二つ受け取り,'a型の結果を返す」という関数の型だ(厳密には前回も説明したように'a -> ('a -> 'a)という意味だが,ここでは二つの引数を受け取る関数の型と考えて良い)。
先の'a -> 'aや'a * 'b -> 'b * 'aの場合と同様に考えると,'a -> 'a -> 'a型の式は以下の2種類しかないように思われる。
# (fun x y -> x : 'a -> 'a -> 'a) ;; - : 'a -> 'a -> 'a = <fun> # (fun x y -> y : 'a -> 'a -> 'a) ;; - : 'a -> 'a -> 'a = <fun>
ただし,この例では単にfun x y -> xやfun x y -> yと書くと,'a -> 'b -> 'aや'a -> 'b -> 'bのように,'a -> 'a -> 'aよりも「一般的」な型が推論されてしまう。そのため(式 : 型)という構文により,わざわざ型を特定している。
# fun x y -> x ;; - : 'a -> 'b -> 'a = <fun> # fun x y -> y ;; - : 'a -> 'b -> 'b = <fun>
もちろん,xとyの型が同じ'aになるのであれば,他の書き方でも良い。
# fun (x : 'a) (y : 'a) -> x ;; - : 'a -> 'a -> 'a = <fun> # fun x y -> (* if式のthenとelseの部分は同じ型になることを利用 *) if true then x else y ;; - : 'a -> 'a -> 'a = <fun>
いずれにせよ,二つの引数を受け取ったら,それらのどちらか一方を返すような関数しかないわけだ。
実際に'a -> 'a -> 'a型の関数が与えられたとき,fun x y -> xとfun x y -> yのどちらであるかは,適当な引数に適用してみればわかる。例えば"a"と"b"という二つの文字列を与えて,"a"が返ってきたらfun x y -> x,"b"が返ってきたらfun x y -> yとわかる。
実は以上のような考え方を応用すると,'aや'bなどの型変数と関数型t1 -> t2および組型t1 * t2だけからなる型を持つ関数については,関数の型と値だけから「ソースコード」を復元することができる。やや難解になってしまうので理屈は省略するが,OCamlで以下の定義を入力してみてほしい(対話環境であれば,全体をコピー&ペーストし,最後に;;をつけてEnterキーを打てば良い)。
let counter = ref 0 let gensym () = incr counter; Printf.sprintf "x%d" !counter type 'a typ = ('a -> string) * (string -> 'a) let val2str (t : 'a typ) (v : 'a) : string = fst t v let str2val (t : 'a typ) (s : string) : 'a = snd t s let z : string typ = (fun v -> v), (fun s -> s) let ( ^-> ) (t1 : 'a typ) (t2 : 'b typ) : ('a -> 'b) typ = (fun f -> let x = gensym () in Printf.sprintf "(fun %s -> %s)" x (val2str t2 (f (str2val t1 x)))), (fun s -> fun x -> str2val t2 (Printf.sprintf "%s %s" s (val2str t1 x))) let ( *^ ) (t1 : 'a typ) (t2 : 'b typ) : ('a * 'b) typ = (fun (v1, v2) -> Printf.sprintf "(%s, %s)" (val2str t1 v1) (val2str t2 v2)), (fun s -> (str2val t1 (Printf.sprintf "fst %s" s), str2val t2 (Printf.sprintf "snd %s" s)))
その上で,ソースコードを復元したい適当な関数(下ではf)を定義する。
# let f (x : 'a) (y : 'a) = x ;; val f : 'a -> 'a -> 'a = <fun>
そうしたら,下のようにval2strという関数に,復元したい関数の型と値を与えてみよう。ただし,型を与えるときは,'aや'bなどの型変数はすべてzという変数に,関数型の->は^->という記号に,組型の*は*^という記号におきかえる。すると,元の関数と等価な関数のソースコード(文字列)が得られるはずだ。
# val2str (z ^-> z ^-> z) f ;; - : string = "(fun x1 -> (fun x2 -> x1))"
もちろん,上の例以外の関数でも同様に動作する。
# let g x y = (y, x) ;; val g : 'a -> 'b -> 'b * 'a = <fun> # val2str (z ^-> z ^-> z *^ z) g ;; - : string = "(fun x3 -> (fun x4 -> (x4, x3)))"
ただし,「ソースコードを復元する」といっても,型と値から再現しているだけなので,変数の名前や無駄な計算まではわからない。例えば,先に出てきた「同じ組を作り直す」例を試すと,以下のように無駄のない関数のソースコードが出力されてしまう。
# let h = fun (x, y) -> let z = (y, x) in (fst z, snd z) ;; val h : 'a * 'b -> 'b * 'a = <fun> # val2str (z *^ z ^-> z *^ z) h ;; - : string = "(fun x5 -> (snd x5, fst x5))"
このことを逆手にとって,プログラム最適化の一種(部分評価)に応用する,という研究もある(参考リンク)。そのような研究(type-directed部分評価という)では,「型変数と関数型と組型だけからなる型を持つ」「副作用などがない」といった制限を緩和するために,いろいろな工夫が考案されている。