用于类型检查类似于 ML 的模式匹配的算法？

Question

对于 ML 风格的编程语言，您如何确定给定模式是否“好”，特别是它是否详尽且不重叠？

假设您有如下模式:

match lst with
  x :: y :: [] -> ...
  [] -> ...

或者:

match lst with
  x :: xs -> ...
  x :: [] -> ...
  [] -> ...

一个好的类型检查器会警告第一个不是详尽的，第二个是重叠的。对于任意数据类型，类型检查器通常如何做出这些决定？

Answer 1

这是一个算法的草图。它也是 Lennart Augustsson 著名的高效编译模式匹配技术的基础。 (paper 出现在令人难以置信的 FPCA 程序 (LNCS 201) 中，点击率如此之高。)这个想法是通过将最一般的模式反复拆分为构造函数案例来重建详尽的、非冗余的分析。

一般来说，问题是你的程序有一堆可能是空的“实际”模式{p1，..，pn}，你想知道它们是否覆盖了给定的“理想”模式q。首先，将 q 作为变量 x。最初满足并随后保持不变的不变量是，每个 pi 都是 σiq，用于某些替换 σi 将变量映射到模式。

如何进行。如果 n = 0，则该束为空，因此您有可能没有被模式覆盖的情况 q。提示 ps 并不详尽。如果 σ1 是变量的单射重命名，那么 p1 会捕获与 q 匹配的所有情况，所以我们很温暖:如果 n=1，我们获胜；如果n>1，那么糟糕，永远不需要p2。否则，对于某个变量 x，σ1x 是构造函数模式。在这种情况下，将问题拆分为多个子问题，每个子问题对应于 x 类型的每个构造函数 cj。也就是说，将原始 q 拆分为多个理想模式 qj = [x:=cj y1 .. yarity(cj)]q，并为每个 qj 相应地细化模式以保持不变量，丢弃不匹配的模式。

让我们以 {[], x :: y :: zs} 为例(将 :: 用于 cons )。我们从

  xs covering  {[], x :: y :: zs}

我们有 [xs := []] 使第一个模式成为理想的实例。所以我们拆分 xs，得到

  [] covering {[]}
  x :: ys covering {x :: y :: zs}

其中第一个是通过空单射重命名来证明的，所以可以。第二个需要 [x := x, ys := y::zs]，所以我们又走了， split ys，得到。

  x :: [] covering {}
  x :: y :: zs covering {x :: y :: zs}

我们可以从第一个子问题中看到我们被banjaxed。

重叠情况更加微妙，并且允许变化，这取决于您是要标记任何重叠，还是仅标记从上到下优先级顺序中完全冗余的模式。你的基本摇滚乐是一样的。例如，从

  xs covering {[], ys}

用 [xs := []] 证明第一个是合理的，所以分开。请注意，我们必须使用构造函数来改进 ys 以保持不变量。

  [] covering {[], []}
  x :: xs covering {y :: ys}

显然，第一种情况严格来说是重叠的。另一方面，当我们注意到需要细化一个实际的程序模式来保持不变性时，我们可以过滤掉那些变得多余的严格细化并检查至少一个存在(就像这里的 :: 案例中发生的那样)。

因此，该算法以一种受实际程序模式 p 驱动的方式构建了一组理想的详尽重叠模式 q。每当实际模式需要特定变量的更多细节时，您就可以将理想模式拆分为构造函数。如果幸运的话，每个实际模式都被不相交的非空理想模式集覆盖，每个理想模式只被一个实际模式覆盖。产生理想模式的案例拆分树为您提供了对实际模式的高效跳转表驱动编译。

我提出的算法显然是终止的，但是如果存在没有构造函数的数据类型，它可能无法接受空的模式集是穷举的。这在依赖类型语言中是一个严重的问题，其中传统模式的详尽性是不确定的:明智的方法是允许“反驳”以及方程式。在 Agda 中，您可以在任何无法改进构造函数的地方编写 ()，发音为“my Aunt Fanny”，这样您就无需使用返回值来完成方程。通过添加足够的反驳，可以使每组详尽的模式都变得详尽无遗。

无论如何，这是基本的图片。