型推論つづき - ラシウラ

http://d.hatena.ne.jp/bellbind/20071121/1195644746

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

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

http://en.wikipedia.org/wiki/Type_inference

型推論のアルゴリズムは「Hindley–Milner type inference algorithm」のとこ
$e \, ::= E \mid v \mid (\lambda v:\tau. e) \mid (e\, e)$
は構文木でVal、Ref、Lambda、Applyに対応する。LetはApplyとLambdaで表現可能だし、複数引数は直積型ということになるので、アルゴリズム上は４つの基本の拡張部分になるだけ。

$\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はマッピングを生成するようにした。保持する問題は、循環参照とか変数型と具体型の区別とかそういうのがいろいろコード上に出てしまうことだったが、マッピングなら対策させやすい。

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