型環境
型環境( type environment)
型環境とは、プログラム中の変数や式に対して、それぞれの型情報を保持する構造のことです。型環境を使うことで、プログラム中でどの変数がどの型を持っているかを追跡できます。これにより、型チェックの際に変数の型情報を利用して型の整合性を確認することができます。
型環境とは
型環境とは、プログラム中の変数や式に対して、それぞれの型情報を保持する構造のことです。型環境を使うことで、プログラム中でどの変数がどの型を持っているかを追跡できます。これにより、型チェックの際に変数の型情報を利用して型の整合性を確認することができます。
型環境の構成
型環境は通常、以下のような形式で表されます:
- ø:空の型環境。初期状態で何も含まれていない状態を示します。
- Γ, x : T:既存の型環境 Γ に、新しい変数 x とその型 T を追加した型環境です。
型環境の拡張の例
以下に具体例を使って説明します。
ステップ1: 初期型環境
まず、初期状態の型環境は空です:
Γ = ø
ステップ2: 変数の追加
ここに新しい変数 x を追加して、その型を int とします。すると、型環境は次のように拡張されます:
Γ = ø, x : int
これは、「変数 x が型 int を持つ」という情報を型環境に追加したことを意味します。
ステップ3: さらに変数を追加
さらに、新しい変数 y を追加して、その型を bool とします。すると、型環境は次のように拡張されます:
Γ = ø, x : int, y : bool
これで、「変数 x が型 int を持ち、変数 y が型 bool を持つ」という情報を型環境に追加したことになります。
拡張された型環境の利用
拡張された型環境は、プログラムの型チェックに利用されます。例えば、以下の式を考えます:
code:.text
x + 1
この式の型チェックを行う際、型環境を参照して x の型を取得し、その型が int であることを確認します。これにより、x + 1 が型 int の式であることを確認できます。
具体的な例
具体的なコード例を示します。例えば、以下のようなプログラムを考えます:
code: .text
lin x : int = 10;
un y : bool = true;
lin fn add(a : lin int, b : lin int) : lin int {
return a + b;
}
add(x, 5);
このプログラムに対する型環境の拡張をステップごとに説明します。
1. 初期型環境:
Γ = ø
2. lin x : int = 10 を処理後:
Γ = ø, x : lin int
3. un y : bool = true を処理後:
Γ = ø, x : lin int, y : un bool
4. 関数定義 lin fn add(a : lin int, b : lin int) : lin int { return a + b; } を処理後:
関数定義のスコープ内では、新しい型環境が作成されます:
Γ_add = ø, a : lin int, b : lin int
5. 関数呼び出し add(x, 5) を処理後:
Γ = ø, x : lin int, y : un bool, add : lin (lin int, lin int) -> lin int
実装例
以下に、Pythonを使った型環境の拡張の実装例を示します。
code:.py
class TypeEnv:
def __init__(self):
self.env = {}
def extend(self, var, typ):
new_env = self.env.copy()
return TypeEnv(new_env)
def lookup(self, var):
return self.env.get(var, None)
def __repr__(self):
return str(self.env)
# 初期型環境
initial_env = TypeEnv()
# 変数 x を追加
env1 = initial_env.extend('x', 'lin int')
print(env1) # {'x': 'lin int'}
# 変数 y を追加
env2 = env1.extend('y', 'un bool')
print(env2) # {'x': 'lin int', 'y': 'un bool'}
# 関数 add を追加
env3 = env2.extend('add', 'lin (lin int, lin int) -> lin int')
print(env3) # {'x': 'lin int', 'y': 'un bool', 'add': 'lin (lin int, lin int) -> lin int'}
このように、型環境を拡張していくことで、プログラム全体の型情報を管理することができます。