型スキーム
「型変数の列」と「型変数を含む型」の対
∀ 型変数の列. 型変数を含む型 というフォーマット実装のイメージ ref
hsdata TypeScheme = Forall [TVar] Type TVar は型変数 Type は、型のASTを表す型例
恒等関数の場合は
∀ a. a->a compose関数の場合は、
∀ a b c. (a -> b) -> (c -> a) -> c -> b 「型スキーム
∀ a.a->a 」と、「自由型変数を用いた型 a->a 」の違い型スキーム
∀ a.a->a 好き勝手に置き換えて良い
多相化されている
自由型変数を用いた型
a->a その時の型環境に依存する
任意に置き換えられるものではない
既に決まっている型のようにして取り扱う
例えば、y:a \vdash \mathrm{let}\;x= y\; \mathrm{in}\;x + 1: \mathrm{int}という式
これは誤りである
型環境内で
y が a 型である時、 let x = y in x + 1 は int 型になると言っているが、
これは
a = int の時でないと成り立たない型環境内の
a がなんであるかに依存するのでこれは誤りになるy:a.a \vdash \mathrm{let}\;x= y\; \mathrm{in}\;x + 1: \mathrm{int}なら成り立つ
これ、同じ記号を使いうるから分かりづらいんだよな
フォント変えたりすればいい
けど、それがむずいから型スキームで表現するのか