Algorithm W Step By Stepを読んだ & 実装した

October 8, 2017

Algorithm WをSwiftで実装してみた。

少し前に作った ukitaka/TypeSystem とほぼ同じだけど、前回のはlet多相を無視して作ったので今回はちゃんと実装。

Algorithm W

Algorithm Wはlet多相をもった型システムにおける型推論アルゴリズム。 TaPLの22章で紹介されているものと違うのは、明示的に型注釈をつけることを許していなくて、完全な型無しラムダ項に主要型を割り当てる。

let多相の動作確認

let id = λ x . x in ((id id) (id 1))

こんなコード相当のテストケースで多相性を確認する。 要は(id id) の左のid(X -> X) -> (X -> X) という型になるが、(id 1)idInt -> Int となって、最終的にこの式全体は Int になることを確認。

func testTypeInference3() {
    let env = TypeEnvironment()
    let x = TypeVariable("x")
    let termX = Term.variable(x)
    let id = TypeVariable("id")
    let termId = Term.variable(id)
    let one = Term.literal(Literal.integer(1))
    let term = Term.let(id, .abstraction(x, termX),
            Term.application(Term.application(termId, termId),  Term.application(termId, one)))
    let inferredType = Inference.typeInference(env: env, term: term)
    XCTAssertEqual(inferredType, .integer)
}

よさそう。

多相性を実現している部分

まずこの部分termBind の型を generalize する。 つまり をつける。

id : X -> X

をこうして、型環境に突っ込んでおく。

id : ∀ X . X -> X 

その後 id が出現して型再構築を行うときに、この部部分 で、フレッシュな型変数に置き換える。TypeSchemeinstantiate がまさにその実装

extension TypeScheme {
    func instantiate() -> Type {
        let freshTypeVariables = (0..<variables.count).map { _ in TypeVariable() }.map(Type.typeVar)
        let subst = Substitution(Dictionary(keys: variables, values: freshTypeVariables))
        return type.apply(subst)
    }
}

おまけ

これを作っている途中にSwiftコミッターのCodaFi氏のAlgorithm.swiftも見つけた。Playgroundで遊ぶならこっちの方がよさそう。

AlgorithmWに加えて、AlgorithmMという推論アルゴリズムを実装している。ちゃんと読んでないけど、AlgorithmWがtop-downなアプローチなのに対して、AlgorithmMがbottom-upなアプローチだとか書いてある。

証明はこっち

このエントリーをはてなブックマークに追加