型推論:「コンピュータ以前」から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など,一般の整数や変数を表す)。

式の構文 直観的な意味
i 整数定数
x 変数参照
( 式1 + 式2 ) 整数加算
( let x = 式1 in 式2 ) 式1の値を変数xにおき,式2の値を計算する
( fun x -> 式 ) 変数xを引数とし,「式」の値を返す関数
( 式1 式2 ) 式1の値を関数として式2の値に適用する

 例えば,下のような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」という型を持つことになる。

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

この先は会員の登録が必要です。有料会員(月額プラン)は初月無料!

日経 xTECHには有料記事(有料会員向けまたは定期購読者向け)、無料記事(登録会員向け)、フリー記事(誰でも閲覧可能)があります。有料記事でも、登録会員向け配信期間は登録会員への登録が必要な場合があります。有料会員と登録会員に関するFAQはこちら