型スキーム
「型変数の列」と「型変数を含む型」の対
∀ 型変数の列. 型変数を含む型というフォーマット
code:hs
data 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
好き勝手に置き換えて良い
多相化されている
その時の型環境に依存する
任意に置き換えられるものではない
既に決まっている型のようにして取り扱う
例えば、$ 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}なら成り立つ
これ、同じ記号を使いうるから分かりづらいんだよなmrsekut.icon
フォント変えたりすればいい
けど、それがむずいから型スキームで表現するのか