如何为OCaml表达式`if true then x else y`构造三种类型环境？

1. 非闭合类型环境 #

非闭合环境的核心是未绑定表达式中的全部自由变量，此表达式的自由变量为x和y，只要环境未绑定其中至少一个变量，就属于非闭合环境。

例子：

• 空环境：Γ = ∅（既未绑定x也未绑定y）
• 仅绑定x的环境：Γ = {x : int}（y未绑定）
• 仅绑定y的环境：Γ = {y : string}（x未绑定）

这类环境下，表达式无法完成完整类型推导，因为存在未绑定的自由变量。

2. 闭合但非良类型的环境 #

闭合环境要求绑定所有自由变量（x和y均在环境中），但非良类型意味着then分支与else分支的类型不匹配，导致整个if表达式无法推导得到合法类型。

例子：

• Γ = {x : int, y : string}：x为整数类型，y为字符串类型，OCaml要求if的两个分支必须为相同类型，因此该环境下表达式类型不合法。
• Γ = {x : bool, y : float}：布尔型与浮点型无法统一，同样属于非良类型的闭合环境。

这类环境中所有变量均已绑定，但分支类型不一致，编译器会抛出类型错误。

3. 闭合且良类型的环境 #

闭合且良类型要求所有自由变量都被绑定，且then和else分支的类型一致，此时整个if表达式的类型即为分支的类型。

例子：

• Γ = {x : int, y : int}：x和y均为整数类型，整个if表达式的类型为int。
• Γ = {x : string, y : string}：x和y均为字符串类型，表达式类型为string。
• Γ = {x : bool, y : bool}：x和y均为布尔类型，表达式类型为bool。

这类环境下，编译器可正常推导出表达式的合法类型，符合OCaml的类型规则。

内容的提问来源于stack exchange，提问作者user832075