什么是OCaml的"地面胁迫"？

Question

OCaml有时会发出警告"这种地面胁迫不是主要的".我想我理解"非主要"部分(类型推断至少给出了两种可能的类型,两者都不是另一种的子类型),但我不知道"地面强制"是什么.

我怀疑答案必须涉及一些抽象类型理论,但我也非常欣赏具体的例子.

Answer 1

以下答案来自Jeremy Yallop.我从OCaml邮件列表中引用它,因为我找不到发布的在线链接.

[tl; dr:消息的意思是"表达式的类型未知.为表达式中的变量添加类型注释."]

背景:私有类型缩写由类型别名定义定义,单词为"private".例如,以下定义

type t = private int

为int做了一些半别名:你可以从类型t转换为int,但你不能从int转换为t.使用':>'运算符执行强制,因此您可以编写类似这样的内容

let f (x : t) = (x :>  int)

从私有类型t转换为缩写类型int.

现在,为了检查以下强制是否有效

(x :> int)

编译器需要知道x的类型.可能有几个候选者:例如,在范围内使用私有类型缩写,如果x具有类型t,则强制有效,但是也不允许强制执行任何强制,因此int是另一种合理的可能性.编译器如何在这些替代方案之间进行选择以找到x的类型？在上面的f的定义中,选择很简单:x是带有注释的函数参数,因此编译器只使用该注释.这是一个稍微棘手的案例:

let g (y : t) = ()

let h x = (g x, (x :> int))

这里的x是什么类型的？编译器的推理算法从左到右检查一对元素,所以这是发生的事情:

1. 最初,当h的类型检查开始时,x的类型是未知的
2. 检查子表达式gx,为x分配类型t,即g的参数类型
3. 检查强制(x:> int),并确定为正确,因为t可以强制转换为int.

但是,如果推理算法从右到左检查了一对元素,我们将得到以下步骤:

最初,当h的类型检查开始时,x的类型是未知的(2)检查强制(x:> int),并且编译器猜测x的类型.在没有其他信息的情况下,它会猜测.(3)检查并拒绝子表达式gx,因为x的类型为int,而不是t.

实际上,如果我们交换对的元素来模拟第二种行为

let h2 x = ((x :> int), g x)

然后强制被拒绝:

let h x = ((x :> int), g x);;
                         ^
Error: This expression has type int but an expression was expected of type t

由于程序不依赖于推理算法使用的特定顺序,因此编译器会发出警告.您可以通过为x绑定绑定来解决警告:

let h (x : t) = (g x, (x :> int))