时间戳

首页 > 解决方案 > 为什么操作数的顺序会影响作用域？

module - 为什么操作数的顺序会影响作用域？

问题描述

我试图理解为什么在一个表达式中接受某个构造函数而不是另一个表达式。我本来希望它在两者都超出范围。我是 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在左侧使用，我不会在右侧收到任何抱怨。为什么会这样？

标签： moduleocaml

解决方案

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

使用显式类型注释，类型检查器可以从类型中选择构造函数，而无需将构造函数带入范围。

例如，

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，因此我们知道Ainf (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 中，类型检查从左到右进行。因此在

... = Top

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

Top = ...

类型检查器正在尝试查找Top没有任何类型信息的构造函数，并且范围内没有构造函数Top。因此它失败并出现Unbound constructor错误。如果您想避免取决于订单，您可以

  • 写出构造函数的全名：
  Snot.Top = ...
  • 使用显式类型注释
(Top: _ Snot.pred) = ...
  • 打开Snot模块。
  Snot.( Top ) = ...
  (* or *)
  let open Snot in Top = ...

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

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

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

这里的“非主体”是指基于类型的消歧结果取决于类型检查的顺序。

推荐阅读