型環境
変数の型に関する仮定
「変数」の型は「変数」を見ただけでは判断できない
変数がどのように導入されたかを知らないとわからない
このことを「型文脈(type context)」とか、「型環境(type environment)」とかと呼んでいる
$ \Gammaで表される
組(変数, 型スキーム)の列
変数→型スキームの写像とも見れる
型スキームに型変数がない場合は、単純化して(変数, 型)と見れるmrsekut.icon
code:hs
newtype TypeEnv = TypeEnv (Map.Map Var TypeScheme)
Varは(型変数ではなく)、通常の変数を表す
例えば、
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{制約}\}
参考