2005年06月10日

MinCaml読解ノート: 型推論

型推論は変数や関数の型を推定する作業であり、既に述べたように構文木の中のType.Varの値を決めていく。

型推論の中核はTyping.gTyping.unifyである。 Typing.gは型環境env (変数の名前→変数の型の写像)と式eを受け取り、式eの型を返す。

Typing.unifyは二つの型を受け取り、それらを一致させる。つまり一方が未定の型変数であれば型が決定する。双方が既知の型であれば一致しない場合にはエラーとなる。

この二つが互いを呼んで再帰的に式や式の内部の変数の型を推論する。

コードにはあまり直接表れないが型推論には自然ある程度の方向がある。特定の型を対象とする演算子からオペランドの型が決まり、変数定義では値から変数の型が決まる。関数本体の式や引数から関数の型が決まり、戻り値の型が決まるという具合である。

Typing.g

定数項であれば型はわかっているのでそれを返す。

not, -, +, *, /, -., +., *., /. では演算子から型が決定できるので、オペランドの型を推論して、その型とunifyする。

==, <= では直ちにオペランドの型はわからないが両辺の型は同じ筈なので、それぞれの推論した型同士をunifyする。式の型としてはType.Boolを返す。 それ以上は両辺の型をチェックしないので、例えばtrue < falseのような式をこの時点でエラーにすることはできない。

if式では、条件の式をType.Boolとunify。then式とelse式をそれぞれ型推論してunifyする。またその型をif式の型として返す。

letでは、=の右辺つまり値の式を型推論したものと型変数をunifyする。これで型変数の中身が決まる筈である(別の型変数を指すだけかも知れないが)。その後、変数名と型変数の組を型環境に追加して、inの後に続く式を型推論する。

let recの場合、まず関数名と関数の型変数を環境に追加する。inに続く式はこの環境を使って推論する。関数本体の式はこれに引数とその型を追加した環境を使って型推論する。

let recの型推論で関数の型変数がどのようになるかの例を挙げる。

let f x = x + 3 in f 4

この式をTyping.gにかけて型推論すると、構文木とその中の型変数は次のようになる。

Syntax.LetRec
 ([{Syntax.name =
     ("f",
      Type.Var
       {contents =
         Some (Type.Fun ([Type.Var {contents = Some Type.Int}], Type.Int))});
    Syntax.args = [("x", Type.Var {contents = Some Type.Int})];
    Syntax.body = Syntax.Add (Syntax.Var "x", Syntax.Int 3)}],
 Syntax.App (Syntax.Var "f", [Syntax.Int 4]))

ついでにletの場合も見てみよう。

let x = 1 in x + 2

この式は次のようになる。

Syntax.Let (("x", Type.Var {contents = Some Type.Int}), Syntax.Int 1,
 Syntax.Add (Syntax.Var "x", Syntax.Int 2))

変数の型推論では、束縛変数であればenvに含まれる筈であるので対応する型変数を返す。envに見付からない場合は外部変数の表であるextenvを捜す。それで見付からない場合は未定義となるが、MinCamlでは宣言のない外部変数を許しており、新しく型変数を与えてextenvに追加する。

関数適用の型推論。関数定義のみでは必ずしもその戻り値は決まらない為、実際に適用して初めて決まる。そこで、その適用における関数の型を表現した値(戻り値の型は未定なので新しい型変数を使う)と、g env eが返す関数の型変数をunifyする。

ここでMinCamlの弱点の一つに遭遇する。関数の型を示す型変数がそのまま使われているため、一度適用でunifyされてしまうと関数の型が固定されてしまい、別の型で呼べなくなる。つまりMinCamlでは関数に多相性がない。例えば次の式は型推論の段階でエラーになってしまう。

let rec f x y = if x < y then 1 else -1 in
print_int (f 3 4) ; print_int (f 2.0 1.0)

回避するには次のように型毎に別々の関数を定義する必要がある。

let rec fi x y = if x < y then 1 else -1 in
let rec ff x y = if x < y then 1 else -1 in
print_int (fi 3 4) ; print_int (ff 2.0 1.0)

型推論がありながらこれでは少し寂しい。言語としてバランスに欠ける。

Typing.unify

2つの型を突き合わせて両者が一致するか調べ、また一致するように型変数を決定する。 つまり片方が未定の型変数であればもう一方の式を代入する。ここが型変数の代入が行われる唯一の箇所である。

このとき、代入する式の中にその型変数が出現していないか調べて循環の発生を防ぐ(と「概説」にはある。だが実際に型が循環するような式はあり得るだろうか?)。

また、両者が既知の型で一致しない場合は例外を発生させる。

Typing.f

Typing.fは型推論のメインルーチンであり、受け取った構文木をTyping.gに渡して型推論する。 その結果とType.Unitをunifyしているのは単なるお節介。様々な式を通して実験するには、このunifyする部分の代わりにコメントアウトされている警告を出力するだけの式を生かすとよい。

Typing.deref_typは型変数をその中身で置き換える関数である。型変数が別の型変数を指している場合はさらにその中身を採る。外部から呼ばれるときに受け取る引数はType.Varであるが、その中身について再帰的に処理するためType.tの全ての型を扱う。

Typing.deref_termは構文木中の型変数を全てその中身で置き換える。

こうして最終的には型変数は実際の型で置き換えられる。

OCamlメモ

例外
例外の宣言: exception 名前 [of 型]
例外の送出: raise 例外
例外の捕捉:
try 式 with 
  パターン -> 式
| パターン -> 式
failwith 文字列
例外Failureを発生させる。
Format.eprintf
エラー出力する関数。
M.add key value map
mapkeyvalueの組を追加する。
M.add_list (key,value)のリスト map
mapに一連の組を追加する。
List.map func list
listの各要素にfuncを適用した結果のリストを返す。
List.iter2 func list1 list2
2つのリストから引数を一つずつとり2引数の関数funcを適用することを繰り返す。
List.exists elem list
リスト中に要素があるか調べる。
この記事へのトラックバックURL
http://blog.seesaa.jp/tb/4251371
※言及リンクのないトラックバックは受信されません。

この記事へのトラックバック
この記事へのコメント
コメントを書く
お名前: [必須入力]

メールアドレス:

ホームページアドレス:

コメント: [必須入力]

認証コード: [必須入力]


※画像の中の文字を半角で入力してください。

広告


この広告は60日以上更新がないブログに表示がされております。

以下のいずれかの方法で非表示にすることが可能です。

・記事の投稿、編集をおこなう
・マイブログの【設定】 > 【広告設定】 より、「60日間更新が無い場合」 の 「広告を表示しない」にチェックを入れて保存する。


×

この広告は1年以上新しい記事の投稿がないブログに表示されております。