Tociyuki::Diary RSSフィード

tociyuki による Perl・Ruby・C++・C で書き散らしたコードを中心に、日常雑記も混在 : B  F  twitter  GitHub  CPAN  本館  公開鍵
 

2016年09月24日

[]Remy の let ランキング法 (遅延法)

Efficient and Insightful Generalization では、 先行法 sound-eager.ml は前フリで、 本命は遅延法の sound-lazy.ml です。 ソースコード中のコメントが充実しているのですが、 まだ理解しきれていません。 それでも、 テストをすべてパスしたので Ruby への直訳を残します。 理解が進んだ段階で、 ruby らしくコードを整えていく予定です。

Remy's let-ranking (lazy) Hindley-Milner type checker

先行法の let ランキング法では、 let 第 1 式の入れ子レベルで型変数をランキングすることで、 効率良く自由型変数集合を扱えるようにしました。 それに加えて、 遅延法では、 型変数だけでなく、 複合型である関数型にも let ランキングをおこなうことで、 型変数の多相型への変更処理と、 多相型から型変数を新しく作成するときの型式の木の複製処理の無駄をなくします。

遅延処理のために前処理と後処理が必要になるため、 型検査のエントリ・ポイントになる手続きが新しく加わります。 DelayedLevelAdjustment は単一化中に後で処理する関数型を記録しておくためのリストです。 今度は単一化中に出現検査から漏れる場合が生じるため、 最後に循環参照が生じていないかどうかを cycle_free でチェックしておきます。

def top_type_check(term)
  TVar.reset
  DelayedLevelAdjustment.reset
  type = typeof(TEnv[], term)
  cycle_free(type)
  type
end

typeof は先行法と同じです。 TEnv と LetLevel も先行法と同じなので省略します。

def typeof(env, term)
  case term
  when Let
    LetLevel.enter
    ty_e = typeof(env, term.exp1)
    LetLevel.leave
    typeof(TEnv.new(term.name, gen(ty_e), env), term.exp2)
  when Var
    type = env.lookup(term.name) or raise InferError, "unbound variable"
    inst(Hash.new, type)
  when Lam
    ty_dom = TVar.new
    ty_cod = typeof(TEnv.new(term.name, ty_dom, env), term.exp)
    TArrow.new(ty_dom, ty_cod)
  when App
    ty_fun = typeof(env, term.exp1)
    ty_dom = typeof(env, term.exp2)
    ty_cod = TVar.new
    unify(ty_fun, TArrow.new(ty_dom, ty_cod))
    ty_cod
  end
end

大域値の DelayedLevelAdjustment は、 promise で処理を後回しにする関数型オブジェクトを @future に記録していき、 force で @current に移して一気に処理を済ませます。 force の最中に、 promise で次回以降に後回しする関数型オブジェクトをさらに登録することができるようにしています。

module DelayedLevelAdjustment
  def self.reset
    @current = []
    @future = []
    self
  end

  def self.promise(arrow)
    @future.unshift arrow
    self
  end

  def self.force
    @current, @future = @future, @current
    @current.each{|arrow| yield arrow }
    @current.clear
    self
  end
end

データ構造では型式の木を構成するオブジェクトから多相型 QVar がなくなって、 多相かそうでないかを TVar と TArrow に直接記録するやりかたへと変わります。 そして、 多相のときは、 入れ子レベルでとりえない大きな定数 GenericLevel を型変数と関数型のレベルにセットします。 オリジナルの説明によると、 この値は実際に OCaml の型検査器で定義している値なのだそうです。

GenericLevel = 100000000

型変数オブジェクトは、 この値を直接持たず、 Unbound オブジェクトでくるんで保持します。 型変数オブジェクトのレベルを変更すると、 Unbound オブジェクトごとさしかえます。 さらに、 型変数は素集合データ構造の要素になり、 素集合の代表要素へのリンクにさしかえることもありえます。

class Type
  def tvar_unbound?() false end     # TVar === type and Unbound === type.content
  def tvar_link?() false end        # TVar === type and Link === type.content
  def tarrow?() false end           # TArrow === type
end

class TVar < Type
  def self.reset
    Gensym.reset
    LetLevel.reset
  end

  attr_reader :content

  def initialize(x = nil)
    @content = x || Unbound.new(Gensym.generate, LetLevel.level)
  end

  def ==(other) TVar === other && @content == other.content end
  def to_s() "TVar#{content}" end
  def polymorphic?() @content.polymorphic? end
  def tvar_unbound?() @content.unbound? end
  def tvar_link?() @content.link? end
  def level() @content.level end

  def change_level(i)
    @content = Unbound.new(@content.name, i)
    i
  end

  def make_link(type)
    @content = Link.new(type)
    type
  end
end

型変数の Unbound オブジェクトで、 レベルを調べて多相かどうかを判定して真理値を返します。 Link オブジェクトは、 リンク先の型が多相かどうかを調べます。

class TVarContent
  def unbound?() false end
  def link?() false end
end

class Unbound < TVarContent
  attr_reader :name, :level
  def initialize(x, n) @name, @level = x, n end
  def ==(other) Unbound === other && @name == other.name && @level == other.level end
  def to_s() "(Unbound #{name.inspect} #{level})" end
  def polymorphic?() GenericLevel == @level end
  def unbound?() true end
end

class Link < TVarContent
  attr_reader :type
  def initialize(ty) @type = ty end
  def ==(other) Link === other && @type == other.type end
  def to_s() "(Link #{type})" end
  def polymorphic?() @type.polymorphic? end
  def link?() true end
end

先行法でもやれば良いのにと思っていた、 素集合データ構造の find 処理は、 遅延法では repr の名称で組み込まれています。 リンクのパスを代表値へのリンクへつけかえながら、 代表値のオブジェクトを返します。

def repr(type)
  if type.tvar_link?
    type.make_link(repr(type.content.type))
  else
    type
  end
end

関数型を let レベルでランキングするために、 2 つの let レベルを記録します。 最初に両方とも現在の let レベルで初期化され、 単一化で @level_new が更新されていき、 @level_old からずれていきます。 そして、 単一化の遅延処理と多相にする gen 処理のときに、 条件を満たしたものを同じ値へと戻します。 どの段階でも、 型変数と同様のランキングを表しているのは @level_new の方です。 なお、 テスト記述用に初期値を Levels 構造体で与えることもできるようにしています。 わざわざ構造体で初期値を指定する形式になっているのは、 OCaml のテスト記述に合わせるためです。 MarkedLevel は型式グラフ構造の探索時に利用します。

MarkedLevel = -1

Levels = Struct.new(:level_new, :level_old)

class TArrow < Type
  attr_reader :dom, :cod
  attr_accessor :level_new, :level_old

  def initialize(d, c, levels = nil)
    levels ||= Levels.new(LetLevel.level, LetLevel.level)
    @dom, @cod, @level_new, @level_old = d, c, levels.level_new, levels.level_old
  end

  def ==(other)
    TArrow === other && @dom == other.dom && @cod == other.cod \
      && @level_new == other.level_new && @level_old == other.level_old
  end

  def to_s() "(#{dom} -> #{cod}, levels{#{level_new}, #{level_old}})" end
  def polymorphic?() GenericLevel == @level_new  end
  def tarrow?() true end
  def marked?() MarkedLevel == @level_new end
  def level() @level_new end

  def set_mark
    i = @level_new
    @level_new = MarkedLevel
    i
  end
end

マークといっても、 型式のグラフ探索中に関数型につけるマークは、 三色マーキング法の灰色マークに相当します。 set_mark はマークで潰す前のランキングの値を返し、 それを探索後にセットしなおして復元させる使い方が基本ですが、 いくつかの探索手続きでは元に戻さず、 別の値に書き換えることもあります。 基本の使い方で一番わかりやすいのは、 循環参照の有無を調べる cycle_free 手続きです。

def cycle_free(type)
  if type.tvar_unbound?
    # do nothing
  elsif type.tvar_link?
    cycle_free(type.content.type)
  elsif type.tarrow?
    if type.marked?
      raise InferError, "occurs check"
    end
    saved_level = type.set_mark
    cycle_free(type.dom)
    cycle_free(type.cod)
    type.level_new = saved_level
  end
end

関数型も let ランキングすることにしたため、 型変数の多相判定をおこなう gen 手続きと、 多相判定されている型変数に対して新しい型変数を生成しながら複製した型式を作成する inst 手続きでは、 多相判定されている関数型だけを走査したり複製するように、 関数型の多相判定が加わります。 それを除くと、 先行法と同じ処理になっています。

def gen(type)
  force_delayed_adjustments     # 単一化中に後回ししておいた関数型の出現検査を済ませる
  gen_loop(type)
  type
end

def gen_loop(type)
  type = repr(type)
  if type.tvar_unbound? and type.level > LetLevel.level
    type.change_level(GenericLevel)
  elsif type.tarrow? and type.level_new > LetLevel.level    # 多相が含まれる関数型
    dom = repr(type.dom)                                    # だけを走査する
    cod = repr(type.cod)
    gen_loop(dom)
    gen_loop(cod)
    type.level_new = type.level_old = [dom.level, cod.level].max
  end
end

def inst(subst, type)
  if type.tvar_unbound? and type.polymorphic?
    subst[type.content.name] ||= TVar.new
  elsif type.tvar_link?
    inst(subst, type.content.type)
  elsif type.tarrow? and type.polymorphic?                  # 多相が含まれている関数型
    TArrow.new(inst(subst, type.dom), inst(subst, type.cod))    # に複製を限定する
  else
    type
  end
end

遅延法の単一化は先行法のものから大幅に変わって、 多相になりうる関数型の出現検査を gen の本処理の直前へと後回しにします。 さらに、 単一化中に関数型へのマーキングを使って検出できる範囲内で循環参照検査をおこないます。

def unify(ty1, ty2)
  return if ty1.equal?(ty2)     # t1 と t2 が同じオブジェクト
  ty1 = repr(ty1)
  ty2 = repr(ty2)
  if ty1.tvar_unbound? and ty2.tvar_unbound?    # 両方とも Unbound な型変数のときは
    if ty1.level > ty2.level                    # ランキングが大きい方を潰して
      ty1.make_link(ty2)                        # 小さい方へリンクします。
    else
      ty2.make_link(ty1)
    end
  elsif ty1.tvar_unbound?                       # 片方が Unbound な型変数のときは
    update_level(ty1.level, ty2)                # もう一方へリンクします。
    ty1.make_link(ty2)
  elsif ty2.tvar_unbound?
    update_level(ty2.level, ty1)
    ty2.make_link(ty1)
  elsif ty1.tarrow? and ty2.tarrow?             # 両方とも関数型のとき
    if ty1.marked? or ty2.marked?
      raise InferError, "cycle occurs check"
    end
    min_level = [ty1.level, ty2.level].min
    ty1.set_mark
    ty2.set_mark
    unify_lev(min_level, ty1.dom, ty2.dom)
    unify_lev(min_level, ty1.cod, ty2.cod)
    ty1.level_new = min_level
    ty2.level_new = min_level
  else
    raise InferError, "type mismatch"
  end
end

def unify_lev(level, ty1, ty2)
  ty1 = repr(ty1)
  update_level(level, ty1)
  unify(ty1, ty2)
end

update_level 手続きが多相になるかもしれない型変数を含む関数型オブジェクトを gen 直前に出現検査するよう遅延リストに加えます。

def update_level(level, type)
  if type.tvar_unbound?
    not type.polymorphic? or raise RuntimeError, "invalid level"
    if type.level > level
      type.change_level(level)
    end
  elsif type.tarrow?
    not type.polymorphic? or raise RuntimeError, "invalid level_new"
    if type.marked?
      raise InferError, "occurs check"
    end
    if type.level_new > level
      if type.level_old == type.level_new
        DelayedLevelAdjustment.promise(type)        # gen 直前に出現検査する
      end
      type.level_new = level
    end
  else
    raise RuntimeError, "cannot happen #{level} #{type.class}"
  end
end

gen の処理をおこなう直前で、 単一化で後回りにしていた関数型オブジェクトの出現検査をおこないます。 adjust_one で後回しリストに登録された関数型オブジェクトの処理を開始します。 関数型オブジェクトごとにマークしてから、 今度は葉まで降りて型変数と関数型のランキングを変更していきます。 両方とも、 先行法の型変数のと同じ判定条件式を使っています。

def force_delayed_adjustments
  DelayedLevelAdjustment.force {|arrow| adjust_one(arrow) }
end

def adjust_one(arrow)
  if arrow.level_old <= LetLevel.level
    DelayedLevelAdjustment.promise(arrow)   # 次回以降に後回し
  elsif arrow.level_old == arrow.level_new
    # 既に更新済み
  else
    saved_level = arrow.set_mark
    adjust_loop(saved_level, arrow.dom)
    adjust_loop(saved_level, arrow.cod)
    arrow.level_new = arrow.level_old = saved_level
  end
end

def adjust_loop(level, type)
  type = repr(type)
  if type.tvar_unbound? and type.level > level
    type.change_level(level)    # 型変数のランキング変更
  elsif type.tarrow? and type.marked?
    raise InferError, "occurs check"
  elsif type.tarrow?
    if type.level_new > level
      type.level_new = level    # 関数型のランキング変更
    end
    adjust_one(type)
  end
end

2016年09月22日

[]Remy の let ランキング法 (先行法)

Remy が OCaml の型検査器のために 1988 年に発見した let ランキング法 (もしくは、 let レベル法) は、 Hindley-Milner の型推論 Algorithm W に必須の自由型変数集合を効率良く扱うための手法です。 素朴な先行法と、 検査と複製を必要になったときに必要な分だけおこなう遅延法があり、 OCaml は先行法をベースにして遅延法を一部採用しています。 他に、 この手法の同類に、 λランキング法が知られており、 SML/NJ が型検査器に採用しています。

Efficient and Insightful Generalization

Efficient ML Type Inference Using Ranked Type Variables (PDF)

上記のリンクの一番目に 3 つコンセプト・コードが置いてあります。 最初に、 自由型変数集合を考慮していない健全でない型検査器、 続いて、 そのコードに let-ランキングを加えることで自由型変数集合を効率良く扱えるようにした先行法の健全な型検査器、 最後に、 OCaml が採用している遅延法の健全な型検査器へと段階を追って、 理解を深めることができるようになっています。 ただし、 OCaml に十分に慣れている人に限ります。 ということで、 Ruby に書き直して、 私にとって読み取りやすくしてみました。 最初の不健全な型検査器は、 先行法の健全な型検査器から let-ランキングの仕掛けを取り除いただけなので、 省略します。

この稿で説明するのは OCaml からの直訳に近い抜粋です。 ロジックは同じですが、 Gist に Ruby らしい記述に再構成したものをあげておきます。

Remy's let-ranking (eager) Hindley-Milner type checker

簡単にするため型式中の複合型は関数だけです。 定義域の型と値域の型でグラフ構造を作ります。

class TArrow < Type
  attr_reader :dom, :cod
  def initialize(d, c) @dom, @cod = d, c end
  def to_s() "(#{dom} -> #{cod})" end
end

型検査は、 抽象構文木を根から葉へと降りては上りを繰り返して型を検査していきます。 そのとき、 let 式中の変数を束縛する値を求める第 1 式の入れ子レベルを型変数の生成時に割り当てていくのが let-ランキング法です。 let 第 1 式の入れ子レベルは引数渡しして更新していく方法もありますが、 Remy の手法では、 大域値をカウンタに使って入れ子レベルを得る書き方になっています。

# env の下で term の型を検査して返します
def typeof(env, term)
  case term
  when Let  # (let name = exp1 in exp2) 式
    # LetLevel 大域値で exp1 の入れ子レベルを追跡します
    LetLevel.enter      # 入れ子レベルを一段深くします
    ty_e = typeof(env, term.exp1)
    LetLevel.leave      # 元のレベルに戻します
    # gen で ty_e 中の型変数 TVar のうち条件を満たすものを多相 QVar に変更します
    typeof(TEnv.new(term.name, gen(ty_e), env), term.exp2)
  when Var  # 変数参照
    type = env.lookup(term.name) or raise InferError, "unbound variable"
    # inst で型式中の多相 QVar を新しく生成した型変数 TVar に置き換えた
    # 型式に変換します
    inst(type)
  when Lam  # (fun name -> exp) ラムダ抽象
    ty_x = TVar.new
    ty_e = typeof(TEnv.new(term.name, ty_x, env), term.exp)
    TArrow.new(ty_x, ty_e)
  when App  # (exp1 exp2) 関数適用
    ty_fun = typeof(env, term.exp1)
    ty_dom = typeof(env, term.exp2)
    ty_cod = TVar.new
    unify(ty_fun, TArrow.new(ty_dom, ty_cod))
    ty_cod
  end
end

LetLevel はシングルトンで、 単なるカウンタです。

module LetLevel
  def self.reset() @level = 1; self end
  def self.level() @level ||= 1 end
  def self.enter() @level = level + 1; self end
  def self.leave() @level = level - 1; self end
end

型変数が素集合データ構造になっているのは同じです。 他の要素を指していないときは Unbound オブジェクトを持ち、 それが let-ランキングを覚えています。 型検査中は、 Unbound を内部で自動的に生成していきます。 一方、 テスト用のオブジェクトを作るときに指定することもできます。 Gensym は a、b、c の順に名前を生成していく大域値です。

class TVar < Type
  def self.reset
    Gensym.reset
    LetLevel.reset
  end

  attr_accessor :content

  def initialize(x = nil)
    @content = x || Unbound.new(Gensym.gensym, LetLevel.level)
  end

  def to_s() "TVar#{content}" end
end

TVar の content 属性になるオブジェクトは、 型変数が素集合の代表要素になっているときの Unbound と、 他の要素へのリンクになっているときの Link の 2 種類があります。

class Unbound < TVarContent
  attr_reader :name, :level
  def initialize(s, n) @name, @level = s, n end
  def to_s() "(Unbound #{name.inspect} #{level})" end
end

class Link < TVarContent
  attr_reader :type
  def initialize(t) @type = t end
  def to_s() "(Link #{type})" end
end

let-ランキングは固定値ではなく、 単一化の最中におこなう出現チェックのときに値が書き換わって小さな値のレベルに戻すことがありえます。 この実装では、 そのとき、 Unbound オブジェクトごとすげかえます。 この置き換えは、 型式中の型変数を自由型変数集合へ追加する操作になっています。

# Unbound 型変数 tvar が、 型式 type に含まれていないことを検査します
# 含まれていたら、 例外を発生します
def occurs(tvar, type)
  if TVar === type and tvar.content.equal?(type.content)
    raise InferError, "occurs check"
  elsif TVar === type and Unbound === type.content
    # 代表値の let-ランキングを小さなレベルに書き換えて自由型変数集合に加えます
    min_level = [tvar.content.level, type.content.level].min
    type.content = Unbound.new(type.content.name, min_level)
  elsif TVar === type and Link === type.content
    occurs(tvar, type.content.type)
  elsif TArrow === type
    occurs(tvar, type.dom)
    occurs(tvar, type.cod)
  end
end

単一化は、 上の出現チェックを使います。 なお、 この単一化手続きは、 オリジナルのテスト・パターンを再利用するために、 条件判定と再帰呼び出しを OCaml 版から直訳しているので、 まだるっこしい書き方になっています。

def unify(t1, t2)
  if t1.equal?(t2)
    # t1 と t2 を同一のオブジェクトに束縛している
  elsif TVar === t1 and Unbound === t1.content
    occurs(t1, t2)      # t1 は t2 に含まれていない
    t1.content = Link.new(t2)
  elsif TVar === t2 and Unbound === t2.content
    occurs(t2, t1)      # t2 は t1 に含まれていない
    t2.content = Link.new(t1)
  elsif TVar === t1 and Link === t1.content
    unify(t1.content.type, t2)
  elsif TVar === t2 and Link === t2.content
    unify(t1, t2.content.type)
  elsif TArrow === t1 and TArrow === t2
    unify(t1.dom, t2.dom)
    unify(t1.cod, t2.cod)
  else
    raise InferError, "type mismatch"
  end
  true
end

let 式の第 1 式の型が求まったら、 それをそのまま型環境に登録するのではなく、 型変数のうち条件を満たすものを多相型に変更した型式へ作り直してから、 登録します。 さて、 typeof 手続きでは、 入れ子レベルを戻してから、 gen をおこなっていることを思いだしましょう。 これが意味するところは、 第 1 式の型検査中に単一化の対象にならずに、 let 入れ子レベルが深いままのランキング付けが残っている型変数を多相型に変更するということです。

#  when Let  # (let name = exp1 in exp2) 式
#    LetLevel.enter
#    ty_e = typeof(env, term.exp1)
#    LetLevel.leave
#    typeof(TEnv.new(term.name, gen(ty_e), env), term.exp2)
#                               ^^^^^^^^^
def gen(type)
  if TVar === type and Unbound === type.content and type.content.level > LetLevel.level
    QVar.new(type.content.name)
  elsif TVar === type and Link === type.content
    gen(type.content.type)
  elsif TArrow === type
    TArrow.new(gen(type.dom), gen(type.cod))
  else
    type
  end
end

多相型を意味する QVar オブジェクトは let-レベルを捨てて識別名だけを記録します。

class QVar < Type
  attr_reader :name
  def initialize(s) @name = s end
  def to_s() "QVar #{name.inspect}" end
end

多相型 QVar は最終的な型式には残らず、 変数参照時に新しく生成した型変数 TVar に置き換わります。 この際、 型変数は QVar の識別名ごとに一つ新しく生成し、 同じ識別名に対しては同じ型変数を使いまわします。 そのためのメモを TSubst に記録しつつ、 型式の複製をおこなっていきます。

#  when Var  # 変数参照
#    type = env.lookup(term.name) or raise InferError, "unbound variable"
#    inst(type)
#    ^^^^^^^^^^
def inst(type)
  inst_loop(TSubst[], type).first
end

def inst_loop(subst, type)
  if QVar === type
    ty_qvar = subst.lookup(type.name)
    if ty_qvar
      [ty_qvar, subst]
    else
      tau = TVar.new
      [tau, TSubst.new(type.name, tau, subst)]
    end
  elsif TVar === type and Link === type.content
    inst_loop(subst, type.content.type)
  elsif TArrow === type
    ty1, subst1 = inst_loop(subst,  type.dom)
    ty2, subst2 = inst_loop(subst1, type.cod)
    [TArrow.new(ty1, ty2), subst2]
  else
    [type, subst]
  end
end

最後に、 型環境と inst が使っている置換表は名前と型をつないだリストにしています。 OCaml 版に合わせてリストにしていますが、 型検査器でレキシカル・スコープな型構築子を考慮しないときは、 Array を使って破壊操作で更新すると書きやすかったりします。 また、 上の subst_loop で使っている subst も非破壊リストで記述するよりも、 前の稿の subst_loop に相当する apply 手続きのやりかたに従って Hash を破壊操作する方が記述はすっきりします。

class TEnvBase
  Nothing = Object.new
  def Nothing.lookup(_) nil end

  def self.[]() Nothing end

  attr_reader :name, :type, :last
  def initialize(k, t, e) @name, @type, @last = k, t, e end

  def lookup(k)
    e = self
    while not e.equal?(Nothing)
      return e.type if e.name == k
      e = e.last
    end
    nil
  end
end

class TEnv < TEnvBase
end

class TSubst < TEnvBase
end

2016年09月19日

[]アルゴリズム W の Cardelli 方式

古典的な型推論を代表する Hindley-Milner によるアルゴリズム W は、 単一化の結果を置換表と元の型集合の組み合わせとする行儀の良い作法で定式化してあります。 それをそのまま実装するのではなく、 変数書き換え方式の単一化の作法で実装しているのが、 Luca Cardelli Basic Polymorphic Typechecking (PDF) です。 これを元に ML4 の式の型推論を書いてみます。 ただし、 いきなり、 C++11 にするのはつらいので、 まずは、 Ruby で試しに書いてみることにします。

Algorithm W on Side-Effect Unification for tiny ML

#!/usr/bin/env ruby

require 'set'

class InferError < TypeError; end

#@<型構成子 TCon を定義します@>
#@<型変数 TVar を定義します@>
#@<抽象構文木の構成子 Term を定義します@>
#@<型環境から型変数を束縛している型を探す lookup を定義します@>
#@<単一化 unify 手続きを定義します@>
#@<型変数の属する素集合の代表要素を探し出す disjoint_set_find を定義します@>
#@<型変数が型に含まれているかどうかを検査する occurs_in? を定義します@>

あらかじめ決まっている基本型と複合型をまとめて型構成子と呼ぶことにします。 基本型である整数型と論理型は型構成子のインスタンスにし、 特異メソッドで型名をくっつけています。 複合型である関数型は型構成子のサブクラスにします。 関数型は定義域 (domain) と値域 (codomain) の型を持っています。 定義域と値域は型構成子であることもあれば、 型変数になっていることもあります。

#@<型構成子 TCon を定義します@>=
class TCon
end

TInt = TCon.new
def TInt.to_s() "int" end
TBool = TCon.new
def TBool.to_s() "bool" end

class TFun < TCon
  attr_reader :dom, :cod
  def initialize(d, c) @dom, @cod = d, c end
  def to_s() "(#{dom} -> #{cod})" end
end

型推論をおこなうと、 find-union 法により素集合データ構造へと、基本型・型構成子・型変数をふるいわけます。分けた後の集合には交わりがありません。 そのような場合、 集合を代表する要素を一つ選んで、 同じ集合の他の要素からリンクします。 このリンクを、 置換表で外部にもつ方式がオリジナルのアルゴリズム W で、 Cardelli の方式は型変数にリンクを直接もたせます。 このリンクは型変数から、 型変数か基本型・複合型へのシンボリックリンクに相当し、 リンクをたどっていった先にある要素が単一化の結果の実態になります。 さらに、 型変数を識別子としてふるまわせるために、 Object#equal?(other) を使います。 これら 2 つの仕掛けは古典的なリネーム方式の Prolog の実装や、 SICP に記載されている単一化の実装と同じです。

#@<型変数 TVar を定義します@>=
class TVar
  @@seq_name = 'a'

  attr_reader :parent

  def initilize
    @parent = nil
    @name = nil
  end

  # 型変数は素集合データ構造を構成します
  def make_set(x)
    @parent = x
  end

  def name
    if @name.nil?
      @name = @@seq_name
      @@seq_name = @@seq_name.succ
    end
    @name
  end

  def to_s
    if parent.nil? then name else parent.to_s end
  end
end

そういえば、 Cardelli のコードを見回しても、 多相を表す Scheme 型がありません。 型推論の結果に残った型変数は多相扱いせよということのようです。

アルゴリズム W は、 深さ優先で抽象構文木の枝先まで潜っていってから後戻りしていきます。 潜っていくときに、 必要な変数に対して型変数を作り、 後戻りしながら単一化で型変数を解いていきます。 Cardelli の方式では、 抽象構文木に潜るときに、 多相扱いしない型変数を集合にいれて受け渡していきます。 ということから、 型推論の入り口は、 抽象構文木の構成子の type_check メソッドです。 このメソッドは、 型チェックに成功したら、 型推論した型式を文字列にして返します。 失敗したときは、 理由を文字列にして返します。

#@<抽象構文木の構成子 Term を定義します@>=
class Term
  def type_check(env)
    type_infer(env, Set[]).to_s
  rescue InferError => e
    e.message
  end
end

#@<変数参照 Ref を定義します@>
#@<整数リテラル ILit と論理リテラル BLit を定義します@>
#@<関数適用 App を定義します@>
#@<プリミティブ適用 Pri を定義します@>
#@<条件式 If を定義します@>
#@<ラムダ抽象 Fun を定義します@>
#@<let 式を定義します@>
#@<let rec 式を定義します@>

項の型推論は type_infer メソッドでおこないます。 このメソッドは型環境、 非多相型変数集合の 2 つの引数をとります。

変数参照の型推論は、 lookup 手続きに丸投げします。 この手続きでは、 多相な型変数をインスタンス化などの下請けを担当します。

#@<変数参照 Ref を定義します@>=
class Ref < Term
  attr_reader :name
  def initialize(s) @name = s end
  def type_infer(env, freetvars) lookup(name, env, freetvars) end
  def to_s() name end
end

リテラルは自分の型構成子を返します。

#@<整数リテラル ILit と論理リテラル BLit を定義します@>=
class ILit < Term
  attr_reader :value
  def initialize(c) @value = c end
  def type_infer(env, freetvars) TInt end
  def to_s() value.to_s end
end

class BLit < Term
  attr_reader :value
  def initialize(c) @value = c end
  def type_infer(env, freetvars) TBool end
  def to_s() value.to_s end
end

関数適用では、 関数と定義域の型推論をまずおこないます。 その上で、 値域に新しく型変数を割り当ててから、 単一化するという Hindley-Millner の規則を書き下します。

#@<関数適用 App を定義します@>=
class App < Term
  attr_reader :exp1, :exp2
  def initialize(e1, e2) @exp1, @exp2 = e1, e2 end

  def type_infer(env, freetvars)
    fun_type = exp1.type_infer(env, freetvars)
    dom_type = exp2.type_infer(env, freetvars)
    cod_type = TVar.new
    unify(fun_type, TFun.new(dom_type, cod_type))
    cod_type
  end

  def to_s() "(#{exp1} #{exp2})" end
end

ML4 のプリミティブ適用は、 二項演算式だけなので簡単です。 左辺と右辺の 2 つの定義域は両方とも整数型なので、 型推論した結果を整数型と単一化します。 加乗算式の値域は整数型、 比較演算式のそれは論理型です。 という型規則を書き下します。

#@<プリミティブ適用 Pri を定義します@>=
class Pri < Term
  attr_reader :op, :exp1, :exp2
  def initialize(o, e1, e2) @op, @exp1, @exp2 = o, e1, e2 end

  def type_infer(env, freetvars)
    e1_type = exp1.type_infer(env, freetvars)
    unify(e1_type, TInt)
    e2_type = exp2.type_infer(env, freetvars)
    unify(e2_type, TInt)
    if '<' == op then TBool else TInt end
  end

  def to_s() "(#{op} #{exp1} #{exp2})" end
end

if 式は条件節の値域を論理型に単一化して、 then 節と else 節の型を単一化します。

#@<条件式 If を定義します@>=
class If < Term
  attr_reader :exp1, :exp2, :exp3
  def initialize(e1, e2, e3) @exp1, @exp2, @exp3 = e1, e2, e3 end

  def type_infer(env, freetvars)
    e1_type = exp1.type_infer(env, freetvars)
    unify(e1_type, TBool)
    e2_type = exp2.type_infer(env, freetvars)
    e3_type = exp3.type_infer(env, freetvars)
    unify(e2_type, e3_type)
    e2_type
  end

  def to_s() "(if #{exp1} then #{exp2} else #{exp3})" end
end

Hindley-Millner のポイントの一つに、 ラムダ抽象の定義域の型変数を非多相扱いで推論を始める特徴があります。 余談ですけど、 ruby の組み込みクラス Hash の merge インスタンスメソッドは非破壊操作なのに、 添付ライブラリ set の Set クラスの merge インスタンス・メソッドは破壊操作だというひっかけがあるので、 使うときはマニュアルをチェックして混同しないようにしないと泣きを見ます。 これまで、 何度、 惑わされたことか。

#@<ラムダ抽象 Fun を定義します@>=
class Fun < Term
  attr_reader :var, :exp
  def initialize(x, e) @var, @exp = x, e end

  def type_infer(env, freetvars)
    dom_type = TVar.new
    e_env = env.merge({var => dom_type})
    e_freetvars = freetvars + [dom_type]
    cod_type = exp.type_infer(e_env, e_freetvars)
    TFun.new(dom_type, cod_type)
  end

  def to_s() "(fun #{var} -> #{exp})" end
end

let 式の束縛変数には非多相縛りはありません。 Scheme では let はラムダ抽象のマクロで本質は同じですが、 ML では型推論で別扱いします。

#@<let 式を定義します@>=
class Let < Term
  attr_reader :var, :exp1, :exp2
  def initialize(x, e1, e2) @var, @exp1, @exp2 = x, e1, e2 end

  def type_infer(env, freetvars)
    e1_type = exp1.type_infer(env, freetvars)
    e_env = env.merge({var => e1_type})
    exp2.type_infer(e_env, freetvars)
  end

  def to_s() "(let #{var} = #{exp1} in #{exp2})" end
end

let rec 式の関数名は関数の型構成子に必ずなるので非多相扱いにしなくても平気なはずですが、 Cardelli の元のやりかたにならって非多相扱いにしています。

#@<let rec 式を定義します@>=
class Letrec < Term
  attr_reader :var, :exp1, :exp2
  def initialize(x, e1, e2) @var, @exp1, @exp2 = x, e1, e2 end

  def type_infer(env, freetvars)
    fun_type = TVar.new
    e_env = env.merge({var => fun_type})
    e_freetvars = freetvars + [fun_type]
    exp1_type = exp1.type_infer(e_env, e_freetvars)
    unify(fun_type, exp1_type)
    exp2.type_infer(e_env, freetvars)
  end

  def to_s() "(letrec #{var} = #{exp1} in #{exp2})" end
end

変数参照の下請け手続き lookup は、 型環境に登録されている型構成子中の多相型変数に対して新しい型変数を割り当てつつ、 型構成子を作り直します。 ちなみに、 全部非多相のときもごっそり作り直してしまう書き方になっているのが微妙ですが、 書き直しせずにそのままのロジックにしています。

#@<型環境から型変数を束縛している型を探す lookup を定義します@>=
def lookup(name, env, freetvars)
  env.key?(name) or raise InferError, "undefined #{name}"
  subst = {}
  apply(subst, env[name], freetvars)
end

def apply(subst, a, freetvars)
  t = disjoint_set_find(a)
  case t
  when TInt, TBool
    t
  when TFun
    TFun.new(apply(subst, t.dom, freetvars), apply(subst, t.cod, freetvars))
  when TVar
    if polymorphic?(t, freetvars)
      subst[t] ||= TVar.new
    else
      t
    end
  else
    raise TypeError, "not type #{t.class}"
  end
end

def polymorphic?(v, freetvars)
  not freetvars.any?{|x| occurs_in?(v, x) }
end

単一化は、 型変数のときは実態をとりだしておいてから、 それらに対しておこないます。 型構成子のときは一致するかどうかをチェックします。 関数の型は定義域と値域の両方を単一化します。 この単一化のやりかたは「コンパイラ―原理・技法・ツール (Information & Computing)」428 ページのものに似ています。 型変数の統合をどのタイミングでおこなうかに違いがあります。 ここの古典的な手法では型変数まで降りきってから循環参照をエラーとし、 そうでないときに型変数を union します。 一方、 ドラゴンブックの手法は、 TFun の単一化の再帰呼び出しの前に、 型式の部分木中の型変数を union してから、 単一化の再帰呼び出しをすることで循環参照があっても単一化が成功するようになっています。

#@<単一化 unify 手続きを定義します@>=
def unify(type1, type2)
  a = disjoint_set_find(type1)
  b = disjoint_set_find(type2)
  if a.equal?(b)   # a.object_id == b.object_id
    # ok
  elsif TVar === a
    occurs_in?(a, b) and raise InferError, "cyclic type inference"
    a.make_set(b)
  elsif TCon === a and TVar === b
    unify(b, a)
  elsif TFun === a and TFun === b
    unify(a.dom, b.dom)
    unify(a.cod, b.cod)
  elsif TCon === a and TCon === b
    raise InferError, "type mismatch #{a} #{b}"
  else
    raise "cannot unify #{a.class} #{b.class}"
  end
end

型変数が属する素集合の代表要素を得ます。 リンクをたどれるだけ辿って、 行き着く先を求めます。 その際、 リンクの途中すべてを代表要素へのリンクへすげ替えます。

#@<型変数の属する素集合の代表要素を探し出す disjoint_set_find を定義します@>
def disjoint_set_find(type)
  if TVar === type and type.parent
    type.make_set (disjoint_set_find(type.parent))
  else
    type
  end
end

型変数が型に再帰的に含まれていないかどうかのチェックは、 ここまでの 2 ヶ所で使われています。 型変数が多相かどうかの判定するときと、 単一化で無限ループを判定するときです。 アルゴリズム W では前者が重要で、 この判定により最も一般的な型を選び出しています。

#@<型変数が型に含まれているかどうかを検査する occurs_in? を定義します@>=
def occurs_in?(a, type)
  b = disjoint_set_find(type)
  if a.equal?(b)   # a.object_id == b.object_id
    true
  elsif TFun === b
    occurs_in?(a, b.dom) || occurs_in?(a, b.cod)
  else
    false
  end
end

ここまでで、 アルゴリズムの実装ができあがりました。 以下は、 動作確認のサンプルです。

まずは、 再帰呼び出し版の階乗計算です。 型チェックに成功し、 int に型推論します。

term = 
Letrec.new("fact", Fun.new("n",
  If.new(
    Pri.new('<', Ref.new("n"), ILit.new(1)),
    ILit.new(1),
    Pri.new('*',
      Ref.new("n"),
      App.new(Ref.new("fact"), Pri.new("+", Ref.new("n"), ILit.new(-1))) ))),
  App.new(Ref.new("fact"), ILit.new(5)) )
puts term.to_s + " : " + term.type_check({})
#=> int

単一化が無限ループになる場合です。 型チェックに失敗します。

term = Fun.new("f", App.new(Ref.new("f"), Ref.new("f")))
puts term.to_s + " : " + term.type_check({})
#=> cyclic type inference

多相の例です。 型変数が型の中に残ります。

term =
Fun.new("f", Fun.new("g", Fun.new("h",
  App.new(Ref.new("g"), App.new(Ref.new("f"), Ref.new("h"))))))
puts term.to_s + " : " + term.type_check({})
#=> ((a -> b) -> ((b -> c) -> (a -> c)))