types - 类型变量和局部抽象类型有什么区别？

Question

我试图了解 OCaml 中本地抽象类型的用途。局部抽象类型与类型变量有何不同？看起来它们具有相同的行为:

(* Type variable *)
# let f (x : 'a) : 'a = x;;
val f : 'a -> 'a = <fun>

(* Locally abstract type *)
# let f (type a) (x : a) : a = x;;
val f : 'a -> 'a = <fun>

Answer 1

统一类型变量和局部抽象类型具有完全不同的行为。

特别是，记住统一类型变量很有用:

• 可以统一，例如

let f (x:'a) (y:'a) : 'a = ()

有效并产生 f: unit -> unit -> unit。

• 在整个顶层定义的范围内。

  例如，变量 'a 在 f 的整个范围内都是相同的(因此具有类型 unit -> unit)

let f x =
   let () = (():'a) in
   (x:'a)

相反，局部抽象类型是:

• 局部抽象，因此它们不能与任何其他类型统一。

  例如，

let f (type a) (x:a) (y:a) : a = ()

产生预期的结果

Error: This expression has type unit but an expression was expected of type a

• 作用域良好，本地类型不能超出其作用域。通常，

let f x =
   let y (type a): a = assert false
   (* let's pretend that we can define such `y` value *) in
   (x:a)

产生预期的超出范围的错误

Error: Unbound type constructor a

由于这些基本的差异行为，本地抽象类型已被扩展以支持类型系统的更高级功能。实际上，本地抽象类型:

• 可用于定义本地模块，因为它们是类型构造函数而不是类型变量

let f (type a) (cmp:a -> a -> int) (x:a list) =
  let module S = Set.Make(struct type t = a let compare = cmp end) in
  x |> S.of_list |> S.elements

• 可以在 GADT 上进行模式匹配时使用局部类型方程进行细化，因为它们具有明确定义的范围:

type _ t =
| Int: int t
| Float: float t
let zero (type a) (x:a t) = match x with
| Int -> 0 (* in this branch a = int *)
| Float -> 0. (* whereas a = float in this one*)