前回,'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部分評価という)では,「型変数と関数型と組型だけからなる型を持つ」「副作用などがない」といった制限を緩和するために,いろいろな工夫が考案されている。