型代入
$ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n] というフォーマット
各型変数$ \alpha_iに、具体型$ \tau_iを代入する、という操作を表す
これはあくまでも「操作」、わかりやすく言えば「関数」なので、適用するまでは何も変化しない
$ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n]\alpha_2 のように、「型代入操作」をなんらかの型に適用することで実際に型代入が行われる
ex. $ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n]\alpha_2=\tau_2
型代入操作を型変数$ \alpha_2に適用すると、具体型$ \tau_2になる
ex. $ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n]\mathrm{int}=\mathrm{int}
型代入操作を具体型intに適用しても何も変わらないのでintのまま
ex. $ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n]\beta=\beta
型変数$ \betaに適用したが、型代入の中に$ \betaが含まれていないので、$ \betaのまま変わらない
e.g. $ \left[\tau_1 / e^{\prime}\right]\left(e_{1} e_{2}\right)=\left(\left[\tau_1 / e^{\prime}\right] e_{1}\right)\left(\left[\tau1 / e^{\prime}\right] e_{2}\right)
関数適用$ e_1e_2に適用した時は、分配できる
e.g. $ \begin{aligned} {\left[\tau_{1} / \alpha_{1}, \ldots, \tau_{n} / \alpha_{n}\right]\left(\tau^{\prime} \rightarrow \tau^{\prime \prime}\right) } &=\left(\left[\tau_{1} / \alpha_{1}, \ldots, \tau_{n} / \alpha_{n}\right] \tau^{\prime}\right) \rightarrow\left(\left[\tau_{1} / \alpha_{1}, \ldots, \tau_{n} / \alpha_{n}\right] \tau^{\prime \prime}\right) \end{aligned}
関数に適用した時も、分配できる
例えば
型スキーム∀ a. a -> aに、
型代入[int/b]を適用すると、
結果は適用前と変わらず∀ a. a -> aになる
例えば、
型スキーム∀ a. a -> aに、
型代入[int/a]を適用すると、
結果は適用前と変わらず∀ a. a -> aになる
注意が必要なのは、型スキーム内に存在するaと、型代入内に存在するaは別ものであるということ
見た目が同じなだけ
例えば、
型スキーム∀ a. a -> bに、
型代入[int/b]を適用すると、
結果は∀ a. a -> intになる(はず)
型環境に型代入を適用する
$ S\Gamma
型代入$ Sを型環境$ \Gammaに適用したもの
これは型環境中の、各型スキームに、型代入を適用したもの
補題
$ \Gamma\vdash e:\tauならば、$ S\Gamma\vdash e:S\tauである
前提
式$ e
型$ \tau
型代入$ S
型代入$ [\tau_1/\alpha_1,\dots,\tau_n/\alpha_n] の記述が冗長なのでこれ全体を$ Sと書いている
証明など
短く書けば
$ [t / s] \Gamma=\{y:[t / s] \sigma \mid y: \sigma \in \Gamma\}
code:hs
type Subst = Map.Map TVar Type
型代入は、TVarにTypeを紐付ける操作の辞書と見れる