算法类型检查ML-like模式匹配？ [英] Algorithm for type checking ML-like pattern matching?

问题描述

你如何确定一个给定的模式是否是好，特别是无论是详尽的，不重叠，对于ML风格的编程语言？

How do you determine whether a given pattern is "good", specifically whether it is exhaustive and non-overlapping, for ML-style programming languages?

假设你有一个这样的模式：

Suppose you have patterns like:

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

或

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

一个很好的类型检查器会警告说，首先是不够详尽，并且第二个是重叠的。如何将类型检查使这些类型的决定在一般情况下，对于任意的数据类型？

A good type checker would warn that the first is not exhaustive and the second is overlapping. How would the type checker make those kinds of decisions in general, for arbitrary data types?

推荐答案

下面是一个算法的草图。这也是伦纳特Augustsson的著名技术有效地编制模式匹配的基础。 （该纸是在令人难以置信的FPCA程序（LNCS 201）用哦，这么多的点击率。）这样做是为了重建一个详尽的，非冗余分析，通过反复分裂最普遍的模式进入构造情况。

Here's a sketch of an algorithm. It's also the basis of Lennart Augustsson's celebrated technique for compiling pattern matching efficiently. (The paper is in that incredible FPCA proceedings (LNCS 201) with oh so many hits.) The idea is to reconstruct an exhaustive, non-redundant analysis by repeatedly splitting the most general pattern into constructor cases.

在一般情况下，问题是，你的程序有可能是空的一堆＆lsquo的，实际的大局;模式{P <子> 1 ，...，P <子> N }，和你想知道他们是否涉及给定的＆lsquo的;理想的大局;图形q。为了揭开序幕，带Q是一个变量x。不变，初步满足，随后维持，是每个P <子>我是与西格玛; <子>我●对于一些替代和西格玛; <子>我映射变量模式

In general, the problem is that your program has a possibly empty bunch of ‘actual’ patterns {p₁, .., p_n}, and you want to know if they cover a given ‘ideal’ pattern q. To kick off, take q to be a variable x. The invariant, initially satisfied and subsequently maintained, is that each p_i is σ_iq for some substitution σ_i mapping variables to patterns.

如何进行。如果n = 0时，一堆是空的，所以你有没有覆盖的模式可能的Q。抱怨PS并非详尽。如果与西格玛; <子> 1 是一个射重命名变量，则P <子> 1 捕捉每个匹配q情况下，所以我们很热情：当n = 1，我们就赢了;如果n> 1，则哎呀，有没有办法P ₂ 可以永远是必要的。否则，我们有一些变量x，＆西格玛; <子> 1 x被构造图案。在这种情况下，分割该问题为多个子问题，每个构造ÇX的类型的<子>Ĵ。也就是说，拆分原始q分成多个理想模式q <子>Ĵ = [X：= C <子>Ĵ是<子> 1 ..是<子>元数（C <子>Ĵ）] Q，并相应完善的模式为每个Q <子>Ĵ维持不变，丢弃那些不匹配。

How to proceed. If n=0, the bunch is empty, so you have a possible case q that isn't covered by a pattern. Complain that the ps are not exhaustive. If σ₁ is an injective renaming of variables, then p₁ catches every case that matches q, so we're warm: if n=1, we win; if n>1 then oops, there's no way p₂ can ever be needed. Otherwise, we have that for some variable x, σ₁x is a constructor pattern. In that case split the problem into multiple subproblems, one for each constructor c_j of x's type. That is, split the original q into multiple ideal patterns q_j = [x:=c_j y₁ .. y_arity(cj)]q, and refine the patterns accordingly for each q_j to maintain the invariant, dropping those that don't match.

让我们用的例子{[]，X ::ÿ:: ZS} （使用 :: 为缺点）。我们先从

Let's take the example with {[], x :: y :: zs} (using :: for cons). We start with

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

和我们有[XS：= []]使第一图案的理想的实例。因此，我们分手XS，让

and we have [xs := []] making the first pattern an instance of the ideal. So we split xs, getting

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

其中第一项是由空射改名有道理，所以就可以了。第二个需要[X：= X，伊苏：= Y :: ZS]，所以我们走了一遍，分裂YS，让

The first of these is justified by the empty injective renaming, so is ok. The second takes [x := x, ys := y :: zs], so we're away again, splitting ys, getting.

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

，我们可以从我们banjaxed第一个子问题见。

and we can see from the first subproblem that we're banjaxed.

重叠的情况下更具隐蔽性，允许变化，这取决于您是否要标记的任何重叠，或者只是模式，这是一个从高端到低端的优先顺序完全是多余的。你的基本摇滚是一样的。例如，以

The overlap case is more subtle and allows for variations, depending on whether you want to flag up any overlap, or just patterns which are completely redundant in a top-to-bottom priority order. Your basic rock'n'roll is the same. E.g., start with

  xs covering {[], ys}

与[XS：= []理由第一的，所以分裂。需要注意的是，我们必须改进YS与构造的情况下保持不变。

with [xs := []] justifying the first of those, so split. Note that we have to refine ys with constructor cases to maintain the invariant.

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

显然，第一种情况是严格意义上的重叠。另一方面，当我们注意到，精炼的实际程序模式是需要维持不变，我们可以过滤掉那些严格精炼即成为多余，并检查中的至少一个生存（如发生在： ：这里的情况）

因此​​，该算法建立在真实动机是实际的程序图案P的方式一套理想的详尽重叠模式Q值。拆分理想的模式为构造情况下，只要实际的模式需要特定变量的更多细节。如果幸运的话，每一个实际的模式覆盖的理想模式不相交的非空子集，每一理想模式覆盖只是一个实际的模式。分裂的情况下其产生理想模式的树给你的实际模式的有效跳转表驱动的编译。

So, the algorithm builds a set of ideal exhaustive overlapping patterns q in a way that's motivated by the actual program patterns p. You split the ideal patterns into constructor cases whenever the actual patterns demand more detail of a particular variable. If you're lucky, each actual pattern is covered by disjoint nonempty sets of ideal patterns and each ideal pattern is covered by just one actual pattern. The tree of case splits which yield the ideal patterns gives you the efficient jump-table driven compilation of the actual patterns.

这个算法我已经presented明确终止，但如果有数据类型，没有构造函数，它可能无法接受的是，空集的模式是面面俱到。这是依赖性类型语言，而传统模式的全面性是不可判定的一个严重的问题：明智的做法是让反驳，以及方程式。在阿格达，你可以写（），读作我的范妮阿姨，在没有构造精细化是可能的任何地方，并且免除您的要求完成与返回值的公式。每一个详尽的一套模式可以做的可辨别的详尽通过足够的反驳增加。

The algorithm I've presented is clearly terminating, but if there are datatypes with no constructors, it can fail to accept that the empty set of patterns is exhaustive. This is a serious issue in dependently typed languages, where exhaustiveness of conventional patterns is undecidable: the sensible approach is to allow "refutations" as well as equations. In Agda, you can write (), pronounced "my Aunt Fanny", in any place where no constructor refinement is possible, and that absolves you from the requirement to complete the equation with a return value. Every exhaustive set of patterns can be made recognizably exhaustive by adding in enough refutations.

总之，这是最基本的图片。

Anyhow, that's the basic picture.

这篇关于算法类型检查ML-like模式匹配？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！