前回「次は再帰型を追加する」と書いたが、その前振りとして関連しているがより簡単な「言語機能としてリスト型を提供する」をまずやっていく。

OCamlでユーザがリスト型を定義するなら：

type 'a list = Nil | Cons of 'a * 'a list

このように代数的データ型を使うことになる。上記の型定義ではまず左型で定義されている'a listが右側の定義の内容にもでてくるのが一つのポイント（再帰型）。そして'a listのように定義される型に型変数が出てくるのもポイント（型コンストラクタによるパラメトリックな型の定義）。

型システムへの拡張としてこれら二つを実装していきたいが、まずTaPLでもSimple Extensionとして扱われている「組み込み型としてのList」の実装。ユーザ定義でないなら再帰型も型コンストラクタも必要ないので楽。

コードはここ。

今回はまず型や式の定義、typeof関数のケースを見ていき、ヘルパ関数などについては次回。

型

組み込みとしてのリスト型は簡単：

type ty =
...
| TList of ty

これで例えばTList TIntは「TInt型の要素を0個以上持つリスト型」を表す。

式

まずはリストを作るための式２つ：

type exp =
...
| ENil
| ECons of exp * exp

ユーザ定義する場合のNil | Cons of 'a * 'a listに対応している。作っている言語内のバリアントのタグとして表現する代わりに、空リストのENilと要素＋リストで新しいリストを作るEConsを言語自体が提供する式として定義している。

次にリストに対する処理：

| EIsNil of exp
| EHead of exp
| ETail of exp

リスト式がENilかどうかを調べるEIsNil、リストの先頭要素をとるEHead、リストの先頭要素以外をとるETailを定義している。

これらはTaPL準拠。TaPLでも「本当だったらパターンマッチで分解する方がいい」と書いてあるが、現在パターンマッチはバリアントにしか対応していないので拡張しようと思ったらややこしくなる。パターンマッチの構文と型システムについては別途書きたい。

定義した式に対する型推論・型検査を見ていく。

まずはENil：

let rec typeof env level = function
...
| ENil -> TList (new_tvar level)

ENilは何らかのリストであることがわかっているが、要素の型がわからない。なので新しく型変数を振って、その「何かまだわからない型」のTListを返す。

ECons：

| ECons(e,elist) ->
  let t = match_list_ty (typeof env level elist) in
  unify (typeof env level e) t;
  TList t

新しく定義するmatch_list_tyというヘルパ関数を使ってelistの型がリスト型である（あるいはそう単一化できる）ことを確認し、そのリスト型の保持する型を返り値として得る（それがt）。先頭要素の型をtと単一化した上でTList tを全体の型として返す。

EIsNil：

| EIsNil e -> ignore (match_list_ty (typeof env level e)); TBool

eがリスト型であることを確認するためにmatch_list_tyを使っている。返ってくる「要素の型」は使わないのでignoreして、全体の型としてはTBoolを返す。

EHead：

| EHead e -> match_list_ty (typeof env level e)

eがリスト型であることを確認し、その要素の型を全体の型として返す。

ETail：

| ETail e -> TList (match_list_ty (typeof env level e))

eがリスト型であることを確認し、その要素の型を保持したTListを全体の型として返す。

次回はmatch_list_tyの定義やis_simpleなどのヘルパ関数を今回定義した式や型にどう対応させるかを見ていく。