OCaml变量类型标注三种写法的差异及适用场景咨询

1. 局部抽象类型写法：let some_fn (type a b) (a : a) (b : b) = ... #

这是**局部抽象类型（Local Abstract Types）**的用法，核心特性：

• 在函数参数列表中声明的a、b是函数体内部的抽象类型，类型检查器不会对它们进行类型统一——也就是说，在函数体内，a和b被视为完全不同、不可互换的类型，彻底避免意外的类型统一。
• 对GADTs至关重要：当函数体内需要匹配GADT构造函数时，局部抽象类型能让类型检查器跟踪GADT构造函数带来的类型细化。比如在处理GADT的不同分支时，局部抽象类型可以保留每个分支的类型约束，不会被提前泛化。

示例（GADT场景）：

type _ expr =
  | Int : int -> int expr
  | Bool : bool -> bool expr

let eval (type a) (e : a expr) : a =
  match e with
  | Int n -> n  // 类型检查器明确此处a=int
  | Bool b -> b // 此处a=bool

这里的(type a)就是局部抽象类型，确保eval能根据GADT的构造函数返回对应类型的值。

2. 显式多态签名写法：let some_fn : type a b . a -> b -> unit = fun a b -> ... #

这是**显式多态（Explicit Polymorphism）**的写法，和局部抽象类型的核心区别在于：

• 它是在函数的签名层面声明多态类型，而非仅在函数体内。这种写法的多态性对外可见，适用于需要明确暴露多态签名的场景。
• 必须使用的场景：当函数作为高阶函数的参数传递，或者GADT的类型约束需要跨函数边界生效时，局部抽象类型的写法无法满足——因为局部抽象的类型仅在函数体内有效，而显式多态签名能让调用方明确感知到函数的多态约束。

示例（高阶函数场景）：

let apply_eval : (type a . a expr -> a) -> a expr -> a =
  fun eval_fn e -> eval_fn e

let my_eval : type a . a expr -> a = fun e ->
  match e with
  | Int n -> n
  | Bool b -> b

let _ = apply_eval my_eval (Int 42)

这里my_eval的显式多态签名是必须的，否则apply_eval无法识别它的多态性。

3. 显式全称量词写法：let fn : 'a 'b . 'a -> 'b -> unit = fun a b -> ... #

这种写法等价于普通的多态函数let fn (a : 'a) (b : 'b) = ...，只是显式写出了全称量词。OCaml默认的多态函数会自动隐式添加全称量词'a 'b .，所以两种写法在语义上完全一致：

• 这里的'a、'b是普通的多态类型变量，类型检查器会根据函数体内的逻辑对它们进行必要的类型统一（如果有需要）。
• 和局部抽象类型的本质区别：普通多态的类型变量可被统一，而局部抽象类型是完全隔离的，不会被统一。

示例：

let fn : 'a 'b . 'a -> 'b -> unit = fun a b -> ()
(* 完全等价于 *)
let fn (a : 'a) (b : 'b) = ()

两者的类型签名完全相同，OCaml的类型推断会自动处理。

内容的提问来源于stack exchange，提问作者David 天宇 Wong