为什么操作数的顺序会影响范围？

Question

我试图理解为什么某个构造函数在一个表达式中被接受，但在另一个表达式中不被接受。我本以为它超出了两者的范围。我是 OCaml 的初学者（我主要使用 Haskell），所以我可能会错过一些对于有经验的人来说完全明显的东西。

type zero = Zero
type 'n succ = Succ
type 'n snat =
  | SZero : zero snat
  | SSucc : 'm snat -> 'm succ snat

module SimpleInduction (Pred : sig type 'n pred end) = struct
  open Pred
  type hyps =
    { base : zero pred
    ; step : 'm. 'm pred -> 'm succ pred}

  let rec induct : type n. hyps -> n snat -> n pred =
          fun h sn -> match sn with
          | SZero -> h.base
          | SSucc p -> h.step (induct h p)
end;;

let module Snot = struct type 'n pred = Top end in
  let module Goop = SimpleInduction(Snot) in
    Goop.induct {base = Top; step = fun _ -> Top} SZero = Top;;
(*
let module Snot = struct type 'n pred = Top end in
  let module Goop = SimpleInduction(Snot) in
    Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
*)

由于某种原因，这个编译得很好。使用未注释的第二个定义Snot，我收到错误：

19 |     Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
         ^^^
Error: Unbound constructor Top

什么纳入Top了第一个定义的范围Snot？使用常规模块而不是一流的本地模块没有什么区别。

如果我Snot.Top在左侧使用，则右侧不会有任何抱怨。这是为什么？

Answer 1

简而言之，类型定向消歧确实不限于范围。

通过显式类型注释，类型检查器可以从类型中选择构造函数，而无需将构造函数引入作用域。

例如，

module M = struct type 'a t = A of 'a end
let ok: _ M.t = A ()
let wrong: _ M.t = A (A ())

第一个示例是有效的，因为类型注释足以知道AinA ()是一个_ A.t. 但是，第二个示例不起作用，因为构造函数尚未带入作用域。

此外，类型定向消歧只需要知道构造函数或记录的预期类型。通常，在本例中

let expected =
  let f (M.A x) = x in
  f (A ())

我们知道 的参数的类型f是 an _ M.t，因此我们知道 inA来自f (A ())，_ M.t并且我们可以使用类型定向消歧，就像使用显式注释的情况一样。

如果您发现这种行为很奇怪，则可以使用警告 42 [name-out-of-scope] 在这种情况下发出警告。编译带有此警告的示例会产生（以及此警告的许多其他实例）

23 |     Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
                                                               ^^^
Warning 40 [name-out-of-scope]: Top was selected from type Snot.pred.
It is not visible in the current scope, and will not 
be selected if the type becomes unknown.

（警告名称是 4.12 中的新名称）

关于第二点，在没有明确注释的情况下，表达顺序可能很重要。事实上，如果没有显式注释，类型定向消歧只能在已知预期类型时选择正确的构造函数。在 OCaml 中，类型检查是从左到右进行的。因此在

let expected =
  let f (M.A x) = x in
  f (A ())

左侧的类型已经被推断出来，因此 的预期类型Top是_ Snot.pred。当顺序颠倒时

23 |     Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
                                                               ^^^
Warning 40 [name-out-of-scope]: Top was selected from type Snot.pred.
It is not visible in the current scope, and will not 
be selected if the type becomes unknown.

类型检查器正在尝试查找没有任何类型信息的构造函数，并且作用域中Top没有构造函数。Top因此它会因Unbound constructor错误而失败。如果您想避免依赖顺序，您可以

• 写出构造函数的全名：

... = Top

• 使用显式类型注释

(Top: _ Snot.pred) = ...

• 打开Snot模块。

Top = ...

我建议使用其中一种解决方案，因为它们更强大。

毕竟，依赖类型检查的具体实现是脆弱的。事实上，有一个编译器标志-principal和一个警告 (18) [非主要]，它会在出现这种潜在的脆弱推理时发出警告：

23 |     Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
                                                               ^^^
Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.

这里“非主要”意味着基于类型的消歧结果取决于类型检查的顺序。