Hatena::ブログ(Diary)

ラシウラ このページをアンテナに追加 RSSフィード Twitter

2007-11-22

型推論つづき

不正確」の解決をしてみる。

一応Wikipediaアルゴリズムがあるので、対応付けしてどこがまずいかチェックしてみる

型推論アルゴリズムは「Hindley–Milner type inference algorithm」のとこ

e ¥, ::= E ¥mid v ¥mid (¥lambda v:¥tau. e) ¥mid (e¥, e)

構文木でVal、Ref、Lambda、Applyに対応する。LetはApplyとLambdaで表現可能だし、複数引数は直積型ということになるので、アルゴリズム上は4つの基本の拡張部分になるだけ。

¥tau ¥, ::= T ¥mid ¥tau ¥to ¥tau

は型構文で、TAtomとTFuncに対応する。

f(¥epsilon , t)というのは、引数は逆だけどinference(expr, table)に対応する。

このルールは構文要素Ref、Apply、Lambdaに対して、分解していくように再帰的に定義する

  • f(¥epsilon, v) = ¥tau where ¥epsilon (v) = ¥tau
  • f(¥epsilon, g¥, e) = ¥tau where f(¥epsilon, g) = ¥tau_1 ¥to ¥tau and f(¥epsilon, e) = ¥tau_1
  • f(¥epsilon, ¥lambda v:¥tau. e) = ¥tau ¥to f(¥epsilon_1, e) where ¥epsilon_1 = ¥epsilon ¥cup (v, ¥tau)

昨日のコード片と比べてみる

    if expr.__class__ is Ref:
        name_type = table.get(expr.name)
        return name_type

    if expr.__class__ is Apply:
        func_type = inference(expr.func, table)
        arg_types = [inference(arg, table) for arg in expr.args]
        ret_type = TVar()
        compare_type = TFunc(arg_types, ret_type)
        try:
            check_type(func_type, compare_type, [])
            if ret_type.concrete is None:
                # parametric
                return ret_type
            else:
                return ret_type.concrete
        except:
            print "Type Error at: %s" % repr(expr)
            raise
        pass

    if expr.__class__ is Lambda:
        table = TypeEnv(table)
        for key in expr.params:
            table.put(key, TVar())
            pass
        body_type = inference(expr.body, table)
        arg_types = [table.get(key) for key in expr.params]
        return TFunc(arg_types, body_type)

変数とか複数引数とかを無視(このあたりが「不正確」部分)すれば、大体同じようになってるのはわかる。

問題はunificationということが必要だということ。これはなにか。

  • u¥, ¥emptyset = ¥mathbf{i}
  • u¥, (¥[¥alpha = T¥] ¥cup C) = u¥, (C’) ¥cdot (¥alpha ¥mapsto T)
  • u¥, (¥[T = ¥alpha¥] ¥cup C) = u (¥[¥alpha = T¥] ¥cup C)
  • u¥, (¥[S ¥to S’ = T ¥to T’¥]¥cup C) = u ¥, (¥{¥[S = T¥], ¥[S’ = T’¥]¥}¥cup C)

uはcheck_typeにあたるところだけど、昨日のコードはここがまずかった。

まずこのuとは何のコードだろうか。uは置き換え関数を生成する関数になってる。不足分を補って単純にpythonで書いてみると以下のようになる:

def merge(pattern, rest):
  "(Type->Type, Type->Type) -> (Type->Type)"
  def merged(type):
    ret = pattern(type)
    return ret if ret is not None else rest(type)
  return merged

def unify(queue):
  "[(Type, Type)] -> (Type->Type)"
  if len(queue) == 0:
    return lambda x: x
  left, right = queue.pop()
  if left.__class__ is TVar:
    func = unify(queue)
    def pattern(type):
      if type == left:
         return right
      else:
         return None
    return merge(pattern, unify(queue))
  if left.__class__ is TFunc and right.__class__ is TFunc:
    queue.append((left.arg_t, right.arg_t))
    queue.append((left.ret_t, right.ret_t))
    return unify(queue)
  if left.__class__ is TAtom and right.__class__ is not TAtom:
    if left.label != right.label:
      raise TypeChechError("mismatched atomic types: %s %s" % (left.label, right.label))
    return unify(queue)
  if right.__class__ is TVar:
    queue.append((right, left))
    return unify(queue)
  raise TypeCheckError("mismatched structure of types: %s %s" % (repr(left), repr(right)))

で、これをどうやって使うか。

  • applyで、check_typeのかわりにtype_map = unify([(left, right)])する。
  • return resolv_type(ret_type, type_map)
    • 変数ret_typeをtype_mapで引く。その結果が関数型の場合、要素にさらに変数型があればさらにtype_mapで引いていき、具体型を作る。

昨日の言語でのAddやTypedとかでは、型が合わない場合、たぶんunifyの時点でエラーが出る。つまりunification結果のマップ関数が作れるかどうかが、型チェックになっている。式の型はその結果のマップ関数を引けばいいことになる。

結局何が問題だったかというと、変数型と具体型とのマッピングをどうとるか。二つの型の構造比較まではよかったけど、その結果を使う必要があり、それをどうやって持てばいいかで間違えた。昨日のコードは構造比較で変数型があったとき保持させた。一方unifyはマッピングを生成するようにした。保持する問題は、循環参照とか変数型と具体型の区別とかそういうのがいろいろコード上に出てしまうことだったが、マッピングなら対策させやすい。

素直に作れたんだなあ。まだ試してないが、明日コードを書き直してみよう。

はてなユーザーのみコメントできます。はてなへログインもしくは新規登録をおこなってください。