型スキームのinstance
型スキーム内の型変数に、具体的な型を代入したものを、instanceと呼んでいる
型変数が具体的な型に実体化しているのでinstanceと言えるmrsekut.icon
型$ \tauと型スキーム$ \sigmaのインスタンス関係を、$ \sigma\succeq \tauと表記する
つまり「型スキーム$ \succeq 型」というフォーマットになる
もっと雑に言うと、「量化された型$ \succeq量化されてない具体的な型」になる
定義
https://gyazo.com/1799c07eb096ce0e916dfbdfbe5e6b55
例えば、
型スキーム: ∀ a b : a -> bで、
型代入: [a/int, b/bool]が存在すると、
この型スキームのinstanceは、int -> boolになる
型スキームには型変数が含まれており、
そこに具体的な型を入れたものをinstanceと呼んでいる
1つの型スキームに対し、複数のinstanceが考えられる
例えば、∀ a. a->aという型スキームのinstanceは、
int -> int
bool -> book
(int -> bool) -> (int -> bool)
など、無限にある