7-1. 型検査と型推論の概要

前節までは、プログラム(式)をどのように評価するか、ということを学んだ。作成した評価器(インタープリタ)は、OCaml と似たような振舞いをするように設計したが、重大な違いの1つが、型の整合性をチェックしない点である。このため、(fun x -> x + 1) true のように、実行するまでもなくエラーであることがわかる式も、処理系は真面目に計算をしてしまい、実行時エラーとなる。 OCaml でこの式を実行しようとすると、コンパイル時の「型推論」によりエラーであることがわかり、早期にディバッグができる。本節(およびそれ以降)では、このための基本となる事項を学ぶ。現代のプログラミング言語の多くは、強力な型システムをもっている。そして、OCaml や C, C++, Java, SML, Haskell, F# などの言語に共通する特徴は，静的な型システムをもっていて、さらに、言語処理系が静的に(コンパイル時に)型の整合性をチェックしてくれることである。 (ちなみに，Scheme/Lisp, Ruby, Perl, JavaScript などのプログラム言語は，動的な型システムを持っている．「動的」というのは，型の整合性のチェックは実行時に(動的に)行われるということである．)

OCaml でプログラミングをした経験のある人は既にわかっているように，型の整合性の検査は非常にありがたく，プログラミング上の小さなエラーはこの検査によって，かなりの程度発見される．この「ありがたみ」がどのような技術によって生み出されているかを見るのが本節の目的である．

本論にはいる前に，型検査と型推論という言葉について整理しておこう． C 言語では，変数の型をプログラム中に明示するので，型の整合性を検査するだけでよい．これは，型検査と呼ばれる．一方，OCamlでは，変数の型をプログラム中に明示しなくてよいので(明示してもよい)，不明な型を推論しつつ整合性を検査することになる．これは型推論という．一般に、型推論の方が型検査より難しい課題である。

タイプ1: 静的な型システムを持ち，静的に型検査を行う; C, Java など．
タイプ2: 静的な型システムを持ち，静的に型推論を行う; OCaml, Haskell, F#など．
タイプ3: 動的な型システムを持つ．Scheme/Lisp, Ruby, Perl, JavaScriptなど．

本実験では、型検査と型推論の基礎となる事項を学ぶ。 OCaml の処理系には、型推論システムが備わっているが、本実験では、型検査システムの作成までを必修課題とし、型推論システムについては発展課題とする。

OCamlでの型の整合性

OCaml の処理系が、どのような式を型が合う(整合的に型を付けられる)と判断しているかは、式を、OCaml処理系に入力してみればわかることである。しかしながら、型が合わなかった場合にOCaml処理系から出力されるエラーメッセージはよくわからないものであることが多いので、どのような場合に型が合うかを系統的に理解しておくことには、意義がある。ここでは、いくつかの例で説明する。

(1 + 3.14) ⇒ 型エラー; 「+」は、OCaml ではint型同士の足し算のみで使う。 float型同士の足し算は「+.」(プラスの記号の後にピリオドがくっついた 2文字) という別の演算子を使う。また、「int型と float型の足し算」という演算はなく、足す前にint型をfloat型に変換することが必要である。

(if true then 10 else "abc") ⇒ 型エラー; (if e1 then e2 else e3) という形の式では、e2 と e3 の型が同じでなければいけない。

(fun x -> match x with true -> 10 | false -> "abc") ⇒ 型エラー; match 式の各ケースで返すものは、全て同じ型でないといけない。

[10; 20; "abc"; 30] ⇒ 型エラー; リストの要素は、全て同じ型でないといけない。

(10, "abc") ⇒ OK; 対(ペア)では、左の部分式と右の部分式が異なる型のものでもよい。これが、リストとは違う点である。

(10, 20, "abc", 3.14, fun x -> x) ⇒ OK; 組(タプル)は、対の一般形であり、組の各要素が違う型でよい。

(if true then 10 else failwith "abc") ⇒ OK; (failwith "...") はどんな型のところにも書くことができる(任意の型を持つ式である。)

(fun x -> if x then x else x + 10) ⇒ 型エラー; これは当然である。

if true then (fun x -> x ^ "abc") "def" else (fun x -> x * 2; "ghi") 10 ⇒ OK; 最初の関数の x と2個目の関数の x は、名前は同じだが、スコープが別であり、別の変数と見なされる。従って、それぞれが異なる型を持ってよい。この場合、 1つ目の関数の x は string型であり、 2つ目の関数の x は int型である。

(fun x -> (x 10) + 20) ⇒ OK; x の型は「整数をもらって整数を返す関数」なので、int->int である。従って、この式全体の型は、(int->int) -> int である。

(fun f -> (fun x -> f (f (x + 10))) ⇒ OK; f: int->int で、x:int である。

(let f = (fun x -> x) in f f) ⇒ OK; これが型が合うのは驚くべきことであるが、多相型 (polymorphic type) のおかげで、型が合う。これについては、OCaml の大きな特徴の1つであるが、本実験の範囲を超えるので、詳細は別の資料を参照してほしい。

トップ, 前へ. 次へ.

亀山幸義