定型环境
 |
定型环境（英语：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，判断结果为假。
相关概念
- 静态类型系统：在编译时进行类型检查的系统。
- 类型推导：在未明确指定类型的情况下，根据程式上下文自动推断类型。
- 类型检查：验证程式中变量或运算是否符合类型规则的过程。