为啥这个 OCaml 定义被错误的类型接受？

Posted 2023-02-19

【中文标题】为啥这个 OCaml 定义被错误的类型接受？

【英文标题】：Why is this OCaml definition accepted with a wrong type?为什么这个 OCaml 定义被错误的类型接受？

【发布时间】：2022-01-20 12:08:29

【问题描述】：

我定义了一个有缺陷的函数：

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> *)

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

【问题讨论】：

OCaml 没有能力表达类型约束“任何不是'b 的'a”。我知道的任何其他语言也没有。如果这不仅仅是一个理论上的问题，绝对没有问题，也许您可​​以尝试在更高的层次上解释您要解决的问题？

我想在写的时候得到异常：let ex56: 'a->'b->'a = fun x y -> x。但不会重写我的代码。

这是不可能的。恐怕在这个抽象级别上没有更多的东西可以提供。

我在想这种类型的函数会限制实现。

可以，但'a -> 'b -> 'a 中表达的唯一约束是第一个参数和返回值必须具有相同的类型。 'a 和 'b 都可以替换为 any 类型，它们没有理由不能是 same 类型。

【参考方案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

使用此注解，类型检查失败并出现错误：

错误：此表达式的类型为 b，但预期的表达式为 a 类型

正如预期的那样。而正确的功能

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

编译没有问题。

这里，前缀type a b. 读作“对于所有可能的类型a 和b”，并且此注释强制f 的类型将等于'a -> 'b -> 'a，没有任何细化（也称为统一）类型变量'a 和'b。

【讨论】：

哈！我没想过为此使用本地抽象类型。这很聪明！但这通常不适用于类型注释，对吗？只是为了函数定义？例如，我不能让高阶函数约束以这种方式传递给它的一等函数？

如果你找到合适的地方来引入局部抽象类型（这对于递归函数来说通常是有问题的），它应该可以工作。但例如，let map (type a b) = let rec map (f:a->b) = function | [] -> [] | x :: l -> f x :: map f l in map 按预期工作

强制函数参数的类型是多态的是高阶多态。这需要在 OCaml 中使用多态记录字段或对象，例如type id = id:'a.'a -> 'a let twice id x = id (id, id x)。

你可以有fst: 'a 'b. 'a -> 'b -> 'a，但是 * 强制执行之间有区别，该函数对 a 和 b 之间的关系一无所知，这可以通过通用量化或局部抽象类型 * 强制执行两种类型不相等，这在 OCaml 中是不可能知道的，因为抽象（即使两个抽象类型可能相等，但相等可能已被模块接口隐藏）

在这里使用本地抽象类型有两个优点：首先，它强制编译器在尝试将抽象类型与不兼容的类型统一时立即发出错误（而不是在检查完整注释时） , 其次使用 GADT 兼容版本有助于减少人们需要记住的句法变化的数量。