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

Question

在官方OCaml文档的"语言扩展"章节的GADT部分中,_ -> .引入了表格的驳斥案例.但是,我认为模式匹配已经是详尽无遗的,所以我不确定何时需要反驳案例.

文档中给出的示例如下:

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'
  | _ -> .

因为typechecker自己添加了一个反驳案例.在4.03引入反驳案例之前,唯一的写法deep是

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

警告8:此模式匹配并非详尽无遗.以下是不匹配的值的示例:
某些_

在那个时间点,没有办法摆脱这个警告(没有禁用它),因为其余的情况在语法上是可能的,但是被某些类型约束禁止.

反驳案件就是为了解决这个问题,在这些简单的情况下会自动添加它们.但在更复杂的情况下,手写的驳斥案件是必要的.例如,如果我从这个功能开始

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 -> .,然后typechecker检查没有任何案例有效.

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

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.

然而,如果你窝足够delays,会出现警告

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

警告8:此模式匹配并非详尽无遗.以下是不匹配的案例:一些(A(A(A(A(A _)))))

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

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