定型环境
 |
定型環境（英語：Typing Environment）是程式語言類型論中的一個重要概念，用於記錄變量名稱及其對應的類型。定型環境通常用符號 Γ（伽瑪）來表示，是靜態類型程式語言中類型檢查和類型推導的基礎工具。
定義
在靜態類型系統中，定型環境是一個映射，用於關聯變量名稱和它們的類型。例如，假設某個定型環境包含以下三個變量：
- x 的類型為整數（int）
- y 的類型為布林值（bool）
- z 的類型為字串（string）
則該定型環境可表示為：
Γ=x:int,y:bool,z:string
其中，冒號「:」用於表示變量與類型的關係。
用途
定型環境在類型系統中的主要用途是確定變量的類型，以支援以下功能：
- 類型檢查：檢查程式中的變量使用是否符合其類型。例如，對於 x 的運算，若定型環境中記錄 x:int，則系統可驗證該變量是否用於整數運算。
- 類型推導：根據上下文推導未知變量的類型，確保程式的類型安全性。
判斷示例
給定定型環境：
Γ=x:int,y:bool,z:string
若需要判斷變量 a 的類型是否為字元（char），可以表示為以下形式：
x:int,y:bool,z:string⊢a:char
此表達式的含義是：在定型環境 Γ 下，驗證 a 的類型是否為 char。由於定型環境中未記錄變量 a，判斷結果為假。
相關概念
- 靜態類型系統：在編譯時進行類型檢查的系統。
- 類型推導：在未明確指定類型的情況下，根據程式上下文自動推斷類型。
- 類型檢查：驗證程式中變量或運算是否符合類型規則的過程。