嵌套模式匹配不是详尽的警告答案

【问题标题】：Nested pattern matching not exhaustive warning嵌套模式匹配不是详尽的警告
【发布时间】：2018-11-07 18:40:53
【问题描述】：

考虑以下代码示例：

function
  | [] -> "bla"
  | ds -> let x::l = List.rev ds in "woot";;

编译/解释上述代码时会出现以下警告：

line 3, characters 14-18:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
[]

我想知道为什么会出现这个警告。很明显，由于顶级模式匹配， [] 不是有效选项。我希望 OCaml 的编译器/解释器能够通过将信息从顶级匹配传递到嵌套匹配来轻松推断出上述代码的详尽性。为什么不是这样？我错过了什么吗？

【问题讨论】：

标签： pattern-matching ocaml

【解决方案1】：

OCaml 在抱怨

let x::l = List.rev ds in "woot"

如果List.rev ds 产生[]，这将失败。

当然，我们知道它不能，因为如果List.rev ds 为空，那么ds 必须为空，这是不可能的，因为有其他守卫；但 OCaml 不知道这一点。

见docs:

OCaml 的模式匹配可以仅根据类型检查一组模式是否详尽。

并继续展示一个与您的非常相似的示例。

关于您的“轻松推断出上述代码的详尽性”......我认为这并不像您说的那么容易。想象一下，如果您要求 ds 不是空的，而是它必须是“foo”，并且内部守卫确保 Digest.to_hex(Digest.string ds) 是 "acbd18db4cc2f85cedef654fccc4a4d8"（必须如此，因为那是"foo" 的 MD5 摘要）。不再那么简单了，即使对我们人类来说也是如此。但是从计算机的角度来看，List.rev ds 和 Digest.to_hex(Digest.string ds) 之间有区别吗？类型很容易。值是硬。

【讨论】：

你回答的例子和我的问题有区别。在您的两个示例中，只有在评估表达式时才能获得信息。在我的例子中， [ ] 只是一个类型构造函数（特别是归纳列表类型的基本情况），这正是对类型推理系统有用的信息。
公平。也许它没有那么那么难。正如引文所示，OCaml 开发人员不想打扰仍然很难。构造函数不是类型，OCaml 无法处理。如果你提出了一个可以做你想做的补丁，我相信他们会很乐意讨论集成它。