Hatena::Grouphaskell

[ pred x | x <- "Ibtlfmm!ojllj" ] RSSフィード

2012-07-10

型システム 08:19

http://www.cafepress.com/skicalc.6225368

Haskellの型システムはHindley-Milner型システムというものに型クラスを加えて拡張したものだそうだ。

一つの式は一つの静的な型を持つ。

GHCだと高階型(複数回ポリモーフする型)や暗黙引数や複数引数型クラスやGADTなどが加わってとても手に負えない有様になっている。

とりあえずHindley-Milnerというものを覚えることにした。

Haskellによる実装があるこの論文をもとにちょこちょこ検索しながら調べる。

出てくる式のようなものは自分の解釈で歪んでいる。記号で書いた日本語として適当に読んでほしい。

推論規則

例によってラムダ計算の式を考える。式の形は「変数参照」と「関数適用」と「関数作成」の3種類。

型システムというのは、下のような論理規則のこと。

[VAR] ((Γ ∪ {var : t}) |- var : t)
[APP] (Γ |- func : a → b) ∧ (Γ |- arg : a) ⇒ (Γ |- (func arg) : b)
[ABS] ((Γ ∪ {arg : a}) |- expr : b) ⇒ (Γ |- (λarg. expr) : a → b)

(Γ |- e : t) は「環境Γ下で式eが型tを持つ」という意味の述語。
Γは { foo : Int, sin : Real -> Real, True : Bool, False : Bool } のような変数名と型を対応づける辞書。
型は (型名) か (型) → (型) のどちらかの形。

これをそのまま実装しても 式 → 型 → Bool のようなチェックする関数が出来上がるだけで、型推論にはならない。

式から型を求めるアルゴリズムは別にあり、広義にはそれも含めてHindley-Milnerと呼ぶ。

let多相

上に載せた規則は不完全で、式も環境もすべて具体型ならいいのだが、id :: a -> a のような多相型(不確定な変数の残っている型)が作れない。

上に[LET]という規則を加えて色々拡張するとHindley-Milnerになる。*1

型ρは単相型τと多相型σのどちらか。
単相型τ は (型名) か τ → ρ のどちらかの形。
多相型 は ∀(型変数名). ρ の形。
関数の型は、引数の方は必ず単相だが、結果のほうの型は多相の可能性がある。

[LET] ((Γ ∪ {generic : σ}) |- expr : τ) ∧ (Γ |poly- generic : σ) ⇒ (Γ |- let generic = expr in body : τ)


ここで Γ |poly- expr : σ というのは |- と別の述語で、単相型ではなく多相型を決める。
|- のほうは単相型を扱う。

規則VARを多相に対応させるため拡張する。

[VAR'] (Γ ⊂ {var : σ}) ∧ (σ ≦ ρ) ⇒ (Γ |- var : ρ)

σ≦ρは「σはρと同じかそれ以上に多相である」ことを表す。

|poly- の定義は以下のとおり。

[SKOL] τ ≦ τ
[SPEC] (substitute(α, τ, σ1) ≦ σ2) ⇒  (∀α. σ1) ≦ σ2
[MONO] τ ≦ τ

[GEN] (α = freetypevariables(ρ) - freetypevariables(Γ))) ∧ (Γ |- expr : t) ⇒ (Γ |poly- expr : ∀α. t)
[INST] (Γ |- expr : ∀α. t) ∧ (τ is a monotype) ⇒ (Γ |- expr : substitute(α, τ, t))

freetypevariables(Γ) = ∪{ freetypevariables(t) | (x : t) ∈ Γ}
freetypevariables(∀α. τ) = freetypevariables(τ) - {α}
freetypevariables(τ) = τ (単相型)

substitute(α, τ, α) = τ
substitute(α, τ, β) = β
substitute(α, τ, x → y) = substitute(α, τ, x) → substitute(α, τ, y)

型の種類が増えて一気に複雑になった。よく見るとGENとINSTは無限ループできるので型推論がさらに難しくなる。

多相型(不確定な変数のある型)a -> aのことで、この規則では∀a. (a -> a)と書く。これは「1階の型」といって、aを与えるとそれが中に代入されて(substitute)0階の単相型になる。(このへんは暗黙)

*1ラムダ計算をSchemeから覚えた自分には「letは抽象+適用の構文糖のはずなのに?」と思えた。「副作用がないのでletをトップレベルdefineの代わりとして使っている」と考えると必要性がすこし飲み込みやすい

トラックバック - http://haskell.g.hatena.ne.jp/illillli/20120710