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

Question

考虑以下代码示例：

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的编译器/解释器能够通过将信息从顶层匹配传递到嵌套匹配，轻松地推断出上述代码的详尽性。为什么不是这样？我是不是遗漏了什么？

Answer 1

OCaml在抱怨

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

如果List.rev ds生成[]，就会失败。

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

请参阅文档

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

然后给出一个与你的例子非常相似的例子。

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