型推論アルゴリズム

• 型推論は，図16.3b で示した型に似た内部表現を使う． そして 2 つの新しい種類の $tys$ も使う．
• 最初は 型メタ変数 である．
  
  $$ty\rightarrow \hbox{\bf Meta}(metavar)$$
  
  メタ変数は，通常の Var 型変数とは異なり Poly により束縛され ない．
• これは，単に unknown 型(推論されることが期待される)のための placeholder に過ぎない．
• 355 ページの append プログラムでは $\alpha,\beta,\gamma$ は，メタ変数であった．
• 変数 $\alpha,\beta,\gamma$ の値を求め，$\delta$ は未決定であっ た．これは，$\delta$ を通常の型変数 d に置き換え， append の型として Poly に束縛される，ことを意味する(多相型)．
• アルゴリズム 16.10 が示すように， function $f(x)=e_1$ の型チェックをする場合，新しいメタ変数 $t_x$ ($x$ の型を意味)と，$t_2$ ($f$ の返答の型を意味)を用意する．
• メタ変数間の関係を処理するために $unify$ を使う．
• 型チェッカは広域環境 $\sigma_m$ (メタ変数をそのインスタンスに マップ)を使う．
• 355 ページでは $\alpha=\hbox{\tt list<}\eta\hbox{\tt >}$ となっ た．これは， バインディング $\alpha\mapsto \hbox{\bf App}(\hbox{\tt list},[\hbox{\bf Meta}(\eta)])$ を $\sigma_m$ に追加することである．
• (しかし)ほとんどの実現では，検索するためのテーブルとして $\sigma_m$ を実現しない．その代わり $\hbox{\bf Meta}(\alpha)$ は，追加 フィールド(最初は，empty) を持つ．
• インスタンシエーションがなされた場合，バインディング $\alpha\mapsto t$ をテーブルに追加する代わりに，$t$ へのポインタを Meta レコードへ格納する．
• アルゴリズム 16.5 の $unify$ 関数に Meta を扱うための 処理を追加する．
• (この説明では)広域環境 $\sigma_m$ にアクセスし，更新する．
  
  $\alpha\in \hbox{domain}(\sigma_m)$
  $unify(\sigma_m(\alpha),t)$

  
  
  
  else if $t\equiv\hbox{\bf App}(\hbox{TyFun}\cdots)$
  
  
  then $unify(\hbox{\bf Meta}(\alpha),\hbox{通常の{\bf TyFun} を展開})$
  
  
  else if $t\equiv\hbox{\bf Meta}(\gamma)\hbox{かつ\}\gamma\in\hbox{domain}(\sigma_m)$
  
  
  then $unify(\hbox{\bf Meta}(\alpha),\sigma_m(\gamma))$
  
  
  else if $t\equiv\hbox{\bf Meta}(\alpha)$
  
  
  then $OK$
  
  
  else if $t$に Meta が出現する．
  
  
  then エラー
  
  
  else $\sigma_m\leftarrow\sigma_m+\{\alpha\mapsto t\}; OK$
  
  $unify(t,\hbox{\bf Meta}(\alpha))=$     $t$ が  Meta でない場合，
  
                  $unify(\hbox{\bf Meta}(\alpha),t)$
  

• メタ変数$\alpha$ がある型$u$ に instantiate されているとす ると，$u$ と $t$ を $unify$ する．それ以外の場合は $\alpha$ を $t$ に instantiate する($\alpha$ を $\alpha$ に instantiate しないよ うに)．
• 節「もし $t$ に Meta が出現したら」は， occurs check という．そして，circular 型を避ける( $\alpha=\hbox{\tt list}<\alpha>$ を instantiate しないようにする(ImplicitPoly-Tiger で は許されない構文である)．
• 型に関する他の関数 - subst と expand のような - では，メタ変数を 「see through」する必要がある．
  $subst(\hbox{\bf Meta}(\alpha),\sigma)=$
  $\alpha\in \hbox{domain}(\sigma_m)$
  $subst(\sigma_m(\alpha),\sigma)$

  
  
  
  else  Meta(

  $\alpha$

  )
  

  $expand(\hbox{\bf Meta}(\alpha))=$
  $\alpha\in \hbox{domain}(\sigma_m)$
  $expand(\sigma_m(\alpha))$

  
  
  
  else  Meta($\alpha$)
  

Generalization と instantiation

• function $f(x)=e_1$ を変換する場合，自由メタ変数を持つ型 で終了する．型 $t_f$ は $\hbox{\bf App}(\hbox{\bf Arrow}, [\hbox{\bf Meta}(\alpha),\hbox{\bf Meta}(\alpha)])$ のようになる． $\alpha$ は，$\sigma_m$ からは instantiate しないとする．
• そのような場合は，以下のように generalize する．
  
  $$\hbox{\bf Poly}([a],\hbox{\bf App}(\hbox{\bf Arrow},[\hbox{\bf Var}(a),\hbox{\bf Var}(a)]))$$
  
  そのため，関数 $f$ はすべての型を適用することができる．
• しかし，注意が必要である．以下のプログラムを考えよう．

  function randomzap(x) =
    let function f(y)=if random() then y else x
    in f
  end

  randomzap の型チェックをする場合， let 式に対して， transexp (これは，$f$ の宣言に対して型チェック) を再帰的に呼び出す 必要がある．
• この位置では $\sigma_v$ における $x$ の型は ${\bf Meta}(\alpha)$ である．しかし generalize できない．
• $f$ は，勝手な型を引数として持つことはできない．$x$ と同じ型の 引数でなければならない．
• この位置では $\alpha$ は (すでに) $x$ の型の記述として，
  現在の環境 $\sigma_v$ に出現する． 従って generalize のアルゴリズムは，以下のようになる．
  $generalize(\sigma_v,t)=$
  $t$

   に出現するメタ変数を 

  $\alpha_1,\alpha_2,\cdots,\alpha_k$

   とする．
  
                      しかし，$\sigma_v$ に出現しない場合，
  
                                  ($\sigma_v$ を検索する場合，メタ変数は $\sigma_m$ を検索する
  
                                  ことにより解釈しなければならない)
  
  
  for $i\leftarrow 1$ to $k$
  
  
  let $\alpha_i\leftarrow \hbox{\tt newtyvar()}$
  
                                  $\sigma_m\leftarrow\sigma_m + \{\alpha_i\mapsto\hbox{\bf Var}(a_i)\}$
  
  
  return  Poly$([a_1,\cdots,a_k],t)$
  

• すべての関数は Poly 型で与えられる．単相関数も Poly$([],\cdots)$ となる．
• generalization の反対は instantiation である． 多相変数が使われた場合，束縛された型変数をメタ変数に置換する．
  $instantiate$

  ( Poly

  $([\alpha_1,\cdots,\alpha_k],t)$

  )=
  
   

  $i\leftarrow 1$

   to $k$
  
                   $\alpha_i\leftarrow\ {\tt newmetavar()}$
  
  
  return $subst(t,\{a_1\mapsto\ \hbox{\bf Meta}(\alpha_1),\cdots,a_k\mapsto\ \hbox{\bf Meta}(\alpha_k)\})$
  

• 多相関数を使うところ各々で， instantiation を処理しなけれ ばならない．
• ある呼ぶ側では，束縛変数 $a_1$ はメタ変数 $\alpha$ ( int に $unify$ される) に置換される．
• 別の呼ぶ側では $a_1$ はメタ変数 $\beta$ ( string に $unify$ される) に置換される．
• またある呼び側では，全ての $\alpha$ の使用に対して，お互いに一致 していなければならない．例えば randomzap 関数は， 多相型 poly<a> a->(a->a) を持つ．以下のように使われる．

  let var i0 := randomzap(0)
      var s0 := randomzap("zero")
    in i0(3)+size(s0("three"))
  end

  これは以下のどれかを返す．$3+5$，$0+5$，$3+4$，$0+4$．
• randomzap の最初の出現では $\alpha\rightarrow(\alpha\rightarrow\alpha)$ ($\alpha$ はメタ変数) と instantiate する．
• しかし，すべての $\alpha$ は $unify$ されなければならない． randomzap(0) の型チェックの場合は $\alpha$ を int に $unify$ する．
• i0(3) の型チェックの場合 は，$\alpha$ を int に $unify$ する．しかし，$\alpha$ は既に int に instantiate されているので，ここでは $\alpha$ が 一貫して使われているか，がチェックされる．
• それから i0(3)+$\cdots$ の型チェックをする場合には， $\alpha$ は再び int に unify される．
• 同様に randomzap の第 2 の出現では， $\beta\rightarrow (\beta\rightarrow\beta)$ と instantiate され，$\beta$ は，すべて string に $unify$ される( size の引数として "zero"， "three" である)．

更新可能変数

• 変数宣言 var a:=$exp$ を考える．変数 a の型を決定す るために $exp$ の型を generalize する．
• a へは初期化を除いて，代入がない場合は sound(健全)であ る．
• しかし，多相的参照(多相型の代入可能な変数)は問題である．以下のプ ログラムは，型チェックを通らない(許されない)．

  let function identity(x) = x
      function increment(i) = i+1
      var a := identity
    in a := increment; a("oops")
  end

• これを安全にするための一つの方法は，更新可能変数の型を generalizing できなくすることである．
• 多相的参照におけるこの制限は，アルゴリズム 16.10 の variable declaration with implicit type で実現されている．