[\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と書いている

証明など

/mrsekut-book-4781912850/165~

短く書けば

[t / s] \Gamma=\{y:[t / s] \sigma \mid y: \sigma \in \Gamma\}

実装のイメージ ref

型代入は、 TVar に Type を紐付ける操作の辞書と見れる