pattern-matching - 在OCaml中什么时候需要驳回案件？

Question

在OCaml官方文档的GADTs section of the "Language extensions" chapter中，引入了_ -> .形式的反驳案例。但是，我认为模式匹配已经十分详尽，因此我不确定何时需要反驳。

该文档中给出的示例如下：

type _ t =
  | Int : int t
  | Bool : bool t

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

但即使是文档，也指出这种驳斥的情况是多余的。是否有一个示例，需要对代码类型检查使用反驳情况？

Answer 1

引用案例对于穷举检查很有用，而不是直接进行类型检查。

您的示例有点令人困惑，因为当模式匹配足够简单时，编译器会自动添加一个简单的引用案例| _ -> .。换一种说法，

let deep : (char t * int) option -> char = function None -> 'c'

相当于

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

因为类型检查器本身会添加一个反驳案例。在4.03中引入驳斥案例之前，写 deep的唯一方法是

let deep : (char t * int) option -> char = function
  | None -> 'c'

警告8：此模式匹配尚未穷尽。

这是一个不匹配的值的示例：

Some _

在那个时候，没有办法消除这个警告（不禁用它），因为其余的情况在语法上是可能的，但是受到某些类型约束的禁止。

引用案例是解决此问题的方法，在这些简单案例中会自动添加它们。但是在更复杂的情况下，手写反驳是必要的。例如，如果我从此功能开始

let either : (float t, char t) result -> char = ...

无法使用正确类型的具体模式来完成省略号 ...：

let either : (float t, char t) result -> char = function
  | Ok Int -> ... (* no, wrong type: (int t, _ ) result *)
  | Ok Bool -> ... (* still no possible (bool t, _) result *)
  | Error Int -> ... (* not working either: (_, int t) result *)
  | Error Bool -> ... (* yep, impossible (_, bool t) result *)

引用案例是一种向类型检查器指示模式的其余案例与现有类型约束不兼容的方法

let either : (float t, char t) result -> char = function
  | Ok _ -> .
  | _ -> .

更确切地说，这些反驳案例告诉编译器尝试扩展案例左侧的所有 _模式，并检查是否无法对这些模式进行类型检查。

通常，在三种情况下需要手写驳斥案：


没有任何可能值的类型上的模式匹配
没有添加自动驳回案例
默认的反例探索深度不够


首先，最简单的玩具示例发生在没有可能的模式时：

let f : float t -> _ = function _ -> .

第二种情况是不符合默认反驳的情况。特别是，仅当 match中有一种情况时才添加驳斥案例：

type 'a ternary = A | B | C of 'a
let ternary : float t ternary -> _ = function
  | A -> ()
  | B -> ()

警告8：此模式匹配尚未穷尽。

这是不匹配的情况的示例：

C _

因此需要一个手写的案例：

let ternary : float t ternary -> _ = function
  | A -> ()
  | B -> ()
  | _ -> .

最后，有时反例的默认探索深度不足以证明没有反例。

默认情况下，探查深度为1：模式_爆炸一次。

例如，在您的示例中，将 | _ -> .转换为 Int | Bool -> .，然后类型检查器检查是否没有大小写有效。

因此，使驳回案例成为必要的一种简单方法是嵌套两个类型的构造函数。例如：

let either : (float t, char t) result -> char = function
  | _ -> .

错误：无法反驳此比赛案件。

这是可以达到的值的示例： _


在这里，必须手动扩展 Ok或 Error情况中的至少一种：

let either : (float t, char t) result -> char = function
  | Ok _ -> .
  | _ -> .

请注意，对于只有一个构造函数的类型有一种特殊情况，展开时仅占完整扩展的1/5。例如，如果您引入一种类型

type 'a delay = A of 'a

然后

let nested : float t delay option -> _ = function
  | None -> ()

很好，因为将 _扩展为 A _的成本为0.2，并且我们仍有一些预算将 A _扩展为 A Int | A Float。

但是，如果嵌套足够的 delay，则会出现警告：

let nested : float t delay delay delay delay delay option -> _ = function
  | None -> ()

警告8：此模式匹配尚未穷尽。

这是不匹配的情况的示例：

Some (A (A (A (A (A _)))))

该警告可以通过添加驳斥案例来解决：

let nested : float t delay delay delay delay delay option -> _ = function
  | None -> ()
  | Some (A _) -> .