型スキームのインスタンス

型スキーム 内の型変数に、具体的な型を代入したものを、instanceと呼んでいる

型変数が具体的な型に実体化しているのでinstanceと言える

型\tauと型スキーム\sigmaのインスタンス関係を、\sigma\succeq \tauと表記する

つまり「 型スキーム \succeq 型 」というフォーマットになる

もっと雑に言うと、「 量化された型 \succeq 量化されてない具体的な型 」になる

定義

例えば、

型スキーム: ∀ a b : a -> b で、

型代入: [a/int, b/bool] が存在すると、

この型スキームのinstanceは、 int -> bool になる

型スキーム には型変数が含まれており、

そこに具体的な型を入れたものをinstanceと呼んでいる

1つの型スキームに対し、複数のinstanceが考えられる

例えば、 ∀ a. a->a という型スキームのinstanceは、

など、無限にある