型推論

• 多相的プログラミングをより簡単にするために，いくつかの多相的言語 - 特に ML と Haskell - は，全く型を指定しなくてもよい．その代わり，型 チェッカが型を推論する．
• 例えば 347 ページにある append を考えてみる．多相レコード 型宣言では <types> を書かないことを除いて，型パラメータは全て書か なければならない．

  
  type list<e>={head:e,tail:list<e>}
  function append(a,b)=
    if a=nil
    then b
    else list{head=a.head,tail=append(a.tail,b)}
  

• このスタイルは多分，より読みやすく，より簡素(concise) に書けるだ ろう．
• どのようにコンパイラは型を推論するのだろう? まず， 型が要求されるところに place-holders $\alpha$，$\beta$，$\gamma$ を挿 入する． function append(a:, b:):=
    if a=nil
    then b
    else list<>head=a.head,tail=append(a.tail,b)
  
• 式 a.head と a.tail に対して a はリストで あるべきで，ある型 $\eta$ に対して $\alpha=$ list<$\eta$> となる． b は， append の結果として返されるので，$\beta=\gamma$ であ ることがわかる． else 節は list<$\delta$> を返すので， $\gamma=$ list<$\delta$> となる．
• 最後に head=a.head のために $\delta=\eta$ であることがわ かる．
• これらの append コードに関する等式を適用すると，コンパイラ は以下のように認識する． function append(a:list<>, b:list<>:list<>=
    if a=nil
    then b
    else list<>{head=a.head, tail=
      append(a.tail,b)}
  

• これは，$\delta$ のある特別な性質に依存しない．そのため， append 関数はすべての型 $\delta$ に対して機能する．
• $\delta$ に対して generalizing することにより，陽に示す型パラメー タを生成する．

  
  function append<d>(a:list<d>,b:list<d>):list<d>=
    if a=nil
    then b
    else list<d>{head=a.head,tail=
      append<d>(a.tail,b)}
  

  347 ページに示した関数と同一である．次のいくつかのページで，型推論 と generalization アルゴリズムを詳しく説明する．