型環境
変数の型に関する仮定
「変数」の型は「変数」を見ただけでは判断できない
変数がどのように導入されたかを知らないとわからない
このことを「型文脈(type context)」とか、「型環境(type environment)」とかと呼んでいる
\Gammaで表される
組
(変数, 型スキーム) の列 変数→型スキーム の写像とも見れる型スキームに型変数がない場合は、単純化して
(変数, 型) と見れる実装のイメージ ref
hsnewtype TypeEnv = TypeEnv (Map.Map Var TypeScheme) Var は(型変数ではなく)、通常の変数を表す TypeScheme は型スキーム例えば、
x: int 、 y: ∀ a. a -> a 、..例:\Gamma \vdash e : \tau
型環境\Gammaのもとで、式eは\tau型ある、ということを表す
「型環境\Gammaのもとで」は式e中の各変数が「型環境で割り当てられた各変数の型に当てはまるならば」という意味
例: \Gamma, x:\tau_1\vdash e:\tau_2
括弧を付けるなら、(\Gamma), (x:\tau_1)\vdash (e:\tau_2)
「現在の型環境\Gammaに、x:\tau_1という宣言を加えた環境」の元で、e:\tau_2である
つまり、xが束縛される値が\tau_1型のものである限り、eの値は\tau_2型である
\Gamma \vdash e : \tau|\phi \{\}
\mathrm{型環境}\vdash\mathrm{式}:\mathrm{型}|\phi\{\mathrm{制約}\}
参考