osiire’s blog

ふしぎなそふとやさん

Algorithm W入門を攻略してきた

先日@pi8027さん著の「Algorithm W入門」を攻略してきました。

http://partake.in/events/22da1e72-032d-49ae-847f-a56606308320

@Mega80bさんに同書をお渡しするついでに読書会です。@t6sさん、@mzpさん、つきあってくれてありがとう。設定したクリア条件は三つ。

  1. 練習問題を全部解くこと
  2. 実装をコンパイル/実行してみること
  3. C{let}とWの違いを説明できること


結局2.は達成できませんでしたが、1.と3.はクリア。せっかくなので3.の説明を書き留めておきます。
まず単純型付けλ計算における型推論は次のステップで実行されます。(この本の方針では)

  1. 項を受け取り、その項の部分項に型付け規則を適用しながら(型と型との)等式の集合を作る。連立方程式みたいなもの。証明木が導出できたらおしまい。
  2. 等式の集合から、その解となる型の割り当てを導く(ユニフィケーション)
  3. 得られた型の割り当てを元の項に適用して、おしまい。


このアルゴリズムにlet多相を入れると次のようになります。(C{let})

  1. 項を受け取り、その項の部分項に型付け規則を適用しながら(型と型との)等式の集合を作る。
    1. ただしlet項の時だけ変数の型が場合によって変わる。let項の型変数のうちlet項の外側の型環境にない型変数は多相にできる。let項の外側の型環境を求めるには、等式の集合をユニフィケーションする。
    2. 多相の変数を型環境から取り出す時にはフレッシュな型変数を割り当てる。
  2. 等式の集合から、その解となる型の割り当てを導く(さらにユニフィケーション)
  3. 得られた型の割り当てを元の項に適用して、おしまい。


これでも目的のlet多相は達成できますが、等式の集合作成時と等式の集合の解を求める時との両方でユニフィケーションが現れます。どうせ等式の集合作成時にユニフィケーションが必要になるなら、もう等式の集合とか作らずに等式が得られるたびに(必要なら)ユニフィケーションしちゃえば、等式の集合を持ちまわって最後にユニフィケーションする必要ないです。

  1. 項を受け取り、その項の部分項に型付け規則を適用して(型と型との)等式を作る。
  2. 等式から(場合によってユニフィケーションを実行して)型の割り当てを導く。証明木が導出できたらおしまい。
    1. let項を多相にするとか、多相な型を環境から取り出す時はフレッシュな型変数を割り当てるとかは前と一緒。
  3. 得られた型の割り当てを元の項に適用して、おしまい。


だいぶすっきりしました。これがアルゴリズムW。