自由型変数のgeneralize

自由型変数を含む型を、型スキームに変換する操作

定義

https://gyazo.com/915d278831e75a527449a7ef621b9938 http://dev.stephendiehl.com/fun/006_hindley_milner.html#generalization-and-instantiation

$ \bar{\alpha}は、型環境$ \Gammaには存在しない自由型変数の名前

例

⊢ e:aの時、⊢ e: ∀ b. bとするような操作

わかりやすく型環境が空の時を考えているmrsekut.icon

⊢の左側が無

式eが、自由型変数a型の時に、

型変数に存在しない型変数名bを導入して、∀ b. bとなるようにgenelizeしている

この時、型環境は無なので、導入する型の名前はaでも良いけど、紛らわしいのでbにしているmrsekut.icon

⊢ e : a->bの時、⊢ e : ∀ c d. c -> dとするような操作

上の例と同じで自由型変数が2つある場合

c, dという型変数名を導入して、∀ c d. c->dとする

これも上と同じでa,bを導入してもいいけど、前後の差が分かりづらいので。

⊢ e : ∀ a. a->bの時、⊢ e : ∀ a c. a -> cとするような操作

aはスキーム化されているため、自由型変数ではない

自由型変数なのはbのみ。

それを踏まえて、上と同じように、cを導入して、∀ a c. a -> cとしている

実装例 ref

code:hs

generalize :: TypeEnv -> Type -> TypeScheme

generalize env t = Forall xs t

where

xs = Set.toList $ ftv t Set.difference ftv env

これは環境依存な実装なので、この関数だけ見ると誤解を生みそうmrsekut.icon

全体で型推論器をつくる際にgenralize関数以外の部分も見ないと整合性が取れない

特に自由型変数の生成部分などに依存する