多相型チェック

• 多相言語の型チェックは，単相型の言語と異なり直接的ではない．
• 実現について説明する前に，型規則は何であるかについてクリアにしよ う．
• Tiger には，(プログラム 5.7 で示した) Types モ ジュールを使った．Poly-Tiger の型を記述するためには，図 16.3 で示す新しい Types モジュールを使う．
• list のような $tycon$ を型パラメータ( <int>) に適用する App 型を持つ．

• 型の内部表現を単純化するために， int をゼロ型引数を持つ 型コンストラクタとする．内部的には ${\bf App}({\bf Int},[])$ と表現す る．
• 2 つの引数を持つ Arrow 型コンストラクタは，関数を示す． $a\rightarrow b$ は ${\bf App}({\bf Arrow},[a,b])$ と表現する．

置換

• 型コンストラクタ ${\bf TyFun}([\alpha_1,\cdots,\alpha_n],t)$ は 型関数を表現する．
• 型$t$ は $\alpha_1,\cdots,\alpha_n$ について言及し，この 型コンストラクタを使った App 型の意味は，$t$ を展開し仮 パラメータ $\alpha_i$ を実型引数に置換することを示す．
• 置換の規則は，アルゴリズム 16.4 で示した．
• 置換の基本的なアイデアは，「型式 $t$ にある $\beta_1$ を $t_1$ に 置換することは，$t$ にあるすべての $\beta_1$ を $t_1$ におき換えること である」．しかし，これは variable capture を避けるために， スコープ規則に従わなければならない．
• もし，型 $t$ が ${\bf Poly}([\beta_1],list<\beta_1>)$ であるとす ると， Poly の仮パラメータ $[\beta_1]$ は，(スコープが Poly の本体である(例えば list$<\beta_1>$)) 新しい変数でなければならない．このスコープの中では，$\beta_1$ の 置換はおきない．
• 式における variable capture の問題点は，節 15.4 (ページ 321) で 述べられている．型置換は，項の置換と同じ方法で，$\alpha-$変換を必要と する．
• capture を避けるためには，アルゴリズム 16.4 において， Poly 規則において新しい変数 $[\gamma_1,\cdots,\gamma_n]$ を用意 した．

型の同等性

• 以下の宣言を考える．

  
  type number=int
  type transformer<e>=e->e
  

  number は，整数 int と同等であり， transformer<int> は， int->int を意味する．これらの型の定義 は，使用目的に合わせて，自由に置換することができる．これを 型の構造的同等性という．
• これら型コンストラクタの内部的な表現は，以下のようになる．
  $$\begin{eqnarray*} \hbox{\tt number} & \mapsto & \hbox{\bf Int}\\ \hbox{\tt tran... ...\hbox{\bf Arrow},\\ & & [\hbox{\bf Var}(e),\hbox{\bf Var}(e)])) \end{eqnarray*}$$
  
  
  
  
  

• Poly-Tiger では，ページ 513 のTiger 言語でのレコード区別 規則を保存したい．各レコード型宣言は「新しい型」を生成する． これは occurrence equivalence of type という¹．
• 以下のように定義できる．

  
  type pair<a>={first:a,second:a}
  type twosome<a>={first:a,second:a}
  

  型 pair<int> と twosome<int> は同じではない．
• 構造的同等(structural equivalence) と occurrence equivalence は，言語設計者の判断である．ML でのレコード型は，例えば，構造的同等を 使う．
• 一般的な Tiger では， Record 型は，フィールド unique という unit ref により区別される．
• しかし，多相言語では，それらを引数として適用する場合に， レコードのディスクリプションをコピーする必要がある．以下のようである．

  
  let type pair<z>={first:z,second:z}
    function f(a:pair<int>):pair<int>=a
   in f
  end
  

• 最初の行では新しい(型ではなく)型コンストラクタ pair を生成 している．パラメータの型としての pair<int> と，結果の型としての pair<int> を同じにしたい．しかし pair<string> は異なった型 としたい．
• pair 型コンストラクタの内部を表現するために以下のように書 くことができる．
  
  $$tycon_p=\hbox{\bf TyFun}([z],\hbox{\bf App}(\hbox{\bf Record}([first, second]),$$
  
  
  
  
  $$[\hbox{\bf Var}(z),\hbox{\bf Var}(z)]))$$
  
  
  しかし，これで pair と twosome を区別しなければならない．
• そこで Unique $tycon$ によりラッピングしよう．
  $$\begin{eqnarray*} tycon_{pair} & = & \hbox{\bf Unique}(tycon_p,q_{323})\\ tycon_{twosome} & = & \hbox{\bf Unique}(tycon_p,q_{324}) \end{eqnarray*}$$
  
  
  
  
  
  タグ $q_{323}$ と $q_{324}$ で pair 型と twosome 型を区別 する．

型同等性のテスト

• しばしば，ある型が他の型と等しいかどうかをテストする必要がある．
• $\hbox{\bf App}(\hbox{\bf TyFun}\cdots,\cdots)$ を含む型をテスト するためには， TyFun の仮パラメータを実パラメータに置換し，展開す る必要がある．
• しかし， $\hbox{\bf App}(\hbox{\bf Unique}(tycon,z),\cdots)$ を含 む型比較のためには，マーク $z$ の uniqueness をテストし， $tycon$ を展開すべきではない．
• アルゴリズム 16.5 で示す $unify$ 関数は， 型の同等性をテストする．
• $error$ に達した場合には，型エラーメッセージをユーザに表示する必 要がある．

Unique 型の展開

• 内部構造を必要とするいくつかの演算を必要とする時， Unique 型の定義の内部を見る必要がある．
• アルゴリズム 16.6 の expand 関数では， TyFun と Unique 型は，内部構造をあばくために展開する．

型の変換

• アルゴリズム 16.7 は， Poly-Tiger 型宣言のシンタックスがどのよ うに，新しい Types モジュールの内部表現に変換されるかを示してい る(全部ではない， Record 型などはなし)．
• 型環境 $\sigma_t$ は，型変数を $ty$ にマップすることを除いて， 識別子を $tycons$ にマップする．
• 型変数は，多相関数で陽に示す型パラメータ， poly 型， パラメータ化された型コンストラクタを扱う，環境で導入される．
• 118 ページの ML コードのように，アルゴリズム 16.7 は，再帰型を扱 うことができない．再帰的に型宣言を扱うためには，119-121 ページに書かれ ているように，最初にヘッダを処理し，その後本体を処理する．
• 通常の Tiger では，再帰宣言を処理する 1st パスが，(2nd パスを処 理するまで右側が満たされない) NAME 型を生成する．
• Poly-Tiger では，2nd パスで満たされる「あな」は Unique 型コンストラクタにあるに違いない( TyFun ではない． Array または Recorad)．

型チェック

• アルゴリズム 16.8 は，宣言の型チェック規則を示す．
• function f<z>(x:$t_1$):$t_2=e_1$ を型チェックするために， 新しい型変数 $\beta$ を生成し，関数パラメータと本体を処理し， z の使用を，正しく認識するために，新しい束縛 z $\mapsto\beta$ を型環境に挿入する． それから仮パラメータは，$\beta$ である Poly 型を生成する．
• 関数呼び出し f<int>$(e_3)$ の型チェックをするために，変数 環境 $\sigma_v$ から $f$ を検索し， $\hbox{\bf Poly}([\beta],\hbox{\bf App}(\hbox{\bf Arrow},[t_1,t_2]))$ を検索する． $t_1$ と $t_2$ にある $\beta$ を int に置換する．
• そして $e_3$ は，型 $t_1$ を持ち，関数呼び出し全体の型として 返答の型 $t_2$ であることをチェックする．
• レコード生成 list<int>{head=x,tail=y} をチェックするた めに $tycon$ を得るために，型環境 $\sigma_t$ にある list を 検索する．
• 結果として，新しいレコード $t_r=\hbox{\bf App}(tycon,t_1)$ を生 成する．それから $t_r$ から head フィールドの型を得ることができ る．そして x の型と $unify$ し，確かめることができる( tail も同様)．