Hindly-Milner 型の表現力

• 多相 append 関数は，Hindly-Milner 型システムを使う言語 ImplicitPoly-Tiger で，2 階のラムダ計算に等しい型システムをもつ Poly-Tiger で書くことができる．
• しかし，実際に ImplicitPoly-Tiger より Poly-Tiger は， (完全に)表現力が高い．
• 以下に示す Poly-Tiger 関数は，ImplicitPoly-Tiger と等しいわけで はない．

  
  function mult(m: poly<a>((a->a)->(a->a)),
    n: poly<b>((b->b)->(b->b))):
      poly<c>(c->c)->(c->c) =
    let function g<d>(f:d->d) : d->d =
    in g
  end
  

• 関数 mult が 陽に示す多相パラメータ m と n を持つ． poly 型を導入するのは，アルゴリズム 16.10 では generalization のみである．また，それは関数定義でのみ出現し， 仮パラメータでは出現しない．
• 一方，ImplicitPoly は，直接 Poly-Tiger に変換することができる． アルゴリズム 16.10 は，型チェックすると同様に，この変換を達成する．
• これは，図 16.1 の 「型推論」というボックスに相当する．
• (関数 mult のような関数を扱う) Poly-Tiger のような型システ ムのための，Hindley-Milner スタイル型推論アルゴリズムは存在しない．
• 2 階のラムダ計算の full な表現力を使うためには，型を full に書か なければならない．
• 特別に Poly-Tiger の表現力が必要かどうかは明らかでない， 陰に型づけされた言語で型推論の利便性の方が，価値が高い．
• 陰に多相型を使う ML と Haskell は，研究コミュニティーにおい て，一般目的のための関数プログラミング言語として成功している．陽に型付 けされた言語でそのような利用をされている言語はない．
• しかし，陽に型付けされた言語は，「多相言語の中間表現」 として位置づけされるようになって来ている．