types - 为什么这个 OCaml 定义接受了错误的类型？

Question

我定义了一个错误函数:

let first : 'a -> 'b -> 'a = fun x y -> y ;;
(* Result: val first : 'a -> 'a -> 'a = <fun> *)

编译器接受它并将类型从 'a->'b->'a 更改为 'a->'a->'a。它不应该工作，因为返回类型应该是 'a，而不是 'b。正确实现:

let first : 'a -> 'b -> 'a = fun x y -> x ;;
(* Result: val first : 'a -> 'b -> 'a = <fun> *)

它为什么起作用以及如何防止编译器像这样更改类型？这成为更复杂表达式的问题。

Answer 1

默认情况下，OCaml 中显式注释中的类型变量是统一变量。特别是，它们可用于添加一些等式约束。例如，x 和 y 共享的 'a 注释允许编译器在

let rec eq (x:'a) (y:'a) = match x, y with
| `Leaf _, `Node _ -> false 
| `Node n1,`Node n2 ->
  eq n1#left n2#left && eq n1#right n2#right 

案例

| _, `Leaf -> ...

丢失了，但如果不将类型变量 'a 精炼为相当复杂的 x 类型，那将无法工作。

问题是注释不是您想要的。如果你想强制一个函数具有多态类型 'a -> 'b -> 'a，你可以使用显式通用量化:

let wrong: type a b. a -> b -> a = fun x y -> y

使用这个注释，类型检查失败并出现错误:

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

如预期。而正确的功能

let ok: type a b. a -> b -> a = fun x y -> x

编译没有问题。

这里，前缀 type a b. 读作“对于所有可能的类型 a 和 b”，这个注解强制f 将等于 'a -> 'b -> 'a 而无需对类型变量 'a 和'b.