型推論：「コンピュータ以前」からML，Java 7まで

　OCamlをはじめ，MLやHaskellなど，多くの型付き関数型言語には型推論という機能がある。この連載でも，暗に陽に，OCamlの型推論機能を利用してきた。

　例えば，以下のような関数say_hello_toを定義してみよう。文字列引数nameを受け取り，nameの前に定数文字列"hello "を付け加えて返す，という関数だ。

# let say_hello_to name = "hello " ^ name ;;
val say_hello_to : string -> string = <fun>

　このように，引数や返り値の型を指定しなくても，say_hello_toはstring ->string型（文字列を受け取り，文字列を返す関数）であると自動推論される。

　ただし，（例えばプログラムを読みやすくするために）もし型を書きたければ，次のように書くこともできる。

# let say_hello_to (name : string) : string = "hello " ^ name ;;
val say_hello_to : string -> string = <fun>

　一般にOCamlでは，(式 : 型)のような構文により，式や引数，返り値などの型を指定することができる。

　また，第6回でも触れたように，モジュールのインタフェースでは，公開する関数の型を書かなくてはならない（ocamlc -iというオプションで自動生成することもできるが）。そのような型は，プログラムの間違いを防いだり実行効率を向上するだけでなく，いわば仕様の一種としても役に立つためだ。

　さて，上のような「型推論」の仕組みは，実はコンピュータやプログラミング言語ができる前から，論理学の分野で研究されていた（参考リンクの"By the way"以降など）。MLやLispといった関数型言語の基礎になった「λ計算」も，元は論理学の体系の一つだ。

　しかし，今や型推論はλ計算や関数型言語だけでなく，C#，C++，Javaといったメジャー言語にも（限られた形ではあるが）取り入れられつつあるという（関連記事，参考リンク1，参考リンク2）。これはジェネリックスやクロージャなど，最近の拡張によって，従来よりも複雑な型が現われてきたためだろう。intやdoubleといった通常の型は良いとしても，多相型（総称型）や高階関数（クロージャ）の型を書くのは本当に面倒だからだ。

　今回は，第10回で考えた単純な関数型言語「MyFun」に対して，もっとも基本的な型推論の一種を実装してみることにしよう。

関数型言語「MyFun」の復習

　第10回で考えたMyFun言語は，多くの関数型言語と同じく，「式」がプログラムであり，式の値を計算すること（評価）がプログラムの実行にあたるのだった。具体的には，MyFunには下のような6種類の式があった（この表でのiやxは，特定の整数や変数ではなく，1，2，-3やx，y，abcなど，一般の整数や変数を表す）。

　例えば，下のようなMyFunのプログラム（式）を実行（評価）すると，10という値が得られる。なぜなら，整数3を変数xにおいてから，「yを受け取るとx+yを返す関数」をfとおき，関数fを整数7に適用するからだ。

(let x = 3 in
 (let f =
    (fun y -> (x + y)) in
  (f 7)))

　実際に，第10回で作ったMyFunインタプリタ（interpret）に上のプログラムを与えてみると，確かに値は10になる。

> ./interpret
(let x = 3 in
 (let f =
    (fun y -> (x + y)) in
  (f 7)))
10

　ちなみに，MyFun言語の構文は（余計な括弧がついているが）OCamlのサブセットになっているので，上述のプログラムはOCamlで実行することもできる。

> ocaml
        Objective Caml version 3.10.0

# (let x = 3 in
   (let f =
      (fun y -> (x + y)) in
    (f 7))) ;;
- : int = 10

　さて，上のようなMyFunプログラムは，OCamlLexとOCamlYaccを利用して生成した字句・構文解析器により，下のように定義されるOCamlのデータ型の値に変換できるのだった。

type var = string

type exp = (* 「式」を表すデータ型 *)
  | Const of int           (* 整数定数 *)
  | Var of var             (* 変数参照 *)
  | Add of exp * exp       (* 整数加算 *)
  | Let of var * exp * exp (* let式 *)
  | Fun of var * exp       (* 関数式 *)
  | App of exp * exp       (* 関数適用 *)

　この字句・構文解析の方法を確認しておこう。まず，第10回に出てきたsyntax.ml，parser.mly，lexer.mllという三つのファイルをocamlcでコンパイルする。

> ocamlyacc parser.mly
> ocamllex lexer.mll
18 states, 957 transitions, table size 3936 bytes
> ocamlc -c syntax.ml parser.mli parser.ml lexer.ml

　すると，次のように，OCamlの対話環境からSyntax，Parser，Lexerの各モジュールを使うことができる。

> ls syntax.cmo parser.cmi parser.cmo lexer.cmo
lexer.cmo  parser.cmi  parser.cmo  syntax.cmo
> ocaml
        Objective Caml version 3.10.0

# #load "syntax.cmo" ;; (* Syntaxモジュールをロード *)
# #load "parser.cmo" ;; (* Parserモジュールをロード *)
# #load "lexer.cmo" ;; (* Lexerモジュールをロード *)
# (* 以下で「Syntax.」の表示を省略するため，Syntaxモジュールをopen *)
  open Syntax ;;
# (* 標準入力から入力されたプログラムを字句・構文解析 *)
  (* MyFunプログラムの部分(let x = 3 in ...)は自分で入力する *)
  let e = Parser.exp Lexer.token (Lexing.from_channel stdin) ;;
(let x = 3 in
 (let f =
    (fun y -> (x + y)) in
  (f 7)))
val e : Syntax.exp =
  Let ("x", Const 3,
   Let ("f", Fun ("y", Add (Var "x", Var "y")),
    App (Var "f", Const 7)))

型を表すデータ型の定義

　さて，「式を表すデータ型」は上のように定義できたので，次に「型を表すデータ型」を定義しよう。MyFun言語には，整数と関数の2種類の値がある。それに合わせて，型も整数型「int」と関数型「t1 -> t2」の2種類が必要になる。ただし，t1 -> t2のt1は引数の型，t2は返値の型だ。また，後で述べる「まだ決まっていない型」を表す「型変数」も含めておく。

　以上をまとめると，「型を表すデータ型」の定義は以下のようになる。

type typ =                 (* 型を表すデータ型 *)
  | TInt                   (* 整数型int *)
  | TFun of typ * typ      (* 関数型t1 -> t2 *)
  | TVar of typ option ref (* 型変数 *)

　例えば，先のMyFunプログラムの変数xは，値が整数3だから，int型を持つはずだ。また，変数yは「x + y」と整数加算に使われているから，やはりint型を持つことになる。すると，fは整数を受け取って整数を返す関数だから，「int -> int」という型を持つことになる。

　このような考え方を一般化すれば型推論が可能になるはずだ。次は，実際の推論アルゴリズムを見てみよう。