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'

Warning 8: this pattern-matching is not exhaustive.

Here is an example of a value that is not matched:
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 -> ()

Warning 8: this pattern-matching is not exhaustive.

Here is an example of a case that is not matched:
C _

因此需要手写案例：

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

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

默认探索深度为1：一个模式_被分解一次。

例如，在您的示例中，| _ -> . 被转换为 Int | Bool -> .，然后类型检查器检查没有任何情况是有效的。

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

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

Error: This match case could not be refuted.

Here is an example of a value that would reach it: _

这里至少需要手动展开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。

然而，如果嵌套足够多 delays，则会出现警告：

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

Warning 8: this pattern-matching is not exhaustive.

Here is an example of a case that is not matched:
Some (A (A (A (A (A _)))))

可以通过添加反驳案例来修复警告：

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

OCaml 什么时候需要反驳案例？

When are refutation cases necessary in OCaml?

pattern-matching

ocaml

gadt