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

Question

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

假设您有以下模式:

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

要么:

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

一个好的类型检查器会警告第一个不是详尽的,第二个是重叠的.对于任意数据类型,类型检查器如何做出一般性的决策？

Answer 1

这是一个算法草图.这也是Lennart Augustsson着名的有效编译模式匹配技术的基础.(该论文涉及令人难以置信的FPCA程序(LNCS 201),其中有很多命中.)这个想法是通过反复将最常见的模式分解为构造函数案例来重建详尽的非冗余分析.

一般来说,问题是你的程序可能有一堆空的"实际"模式{p ₁,..,p _n },并且你想知道它们是否涵盖给定的"理想"模式q.要开始,请将q作为变量x.不变,最初满意并随后保持,是每个p _我是σ _我一些替代σq _我将变量映射到图案.

如何进行.如果n = 0,则束为空,因此您可能有一个未被模式覆盖的情况q.抱怨ps并非详尽无遗.如果σ ₁是一个射重命名的变量,则P _1个捕获每个匹配q的情况下,所以我们很温暖:如果n = 1,我们赢了; 如果n> 1然后哎呀,那就不可能需要p _2了.否则,我们有一些变量x,σ ₁ x是一个构造模式.在这种情况下,将问题拆分为多个子问题,每个子问题对应于x的类型的每个构造函数c _j.也就是说,将原始q分成多个理想模式q _j = [x:= c _j y ₁ ... y _{arity(c j)} ] q,并相应地细化每个q _j的模式以保持不变量,丢弃那些不匹配.

让我们以{[], x :: y :: zs}(使用::for cons)为例.我们一开始

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

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

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

第一个是空的内射重命名,所以没问题.第二个需要[x:= x,ys:= y :: zs],所以我们再次离开,分裂ys,得到.

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

我们可以从第一个子问题看到我们被禁止了.

重叠情况更加微妙,允许变化,具体取决于您是否要标记任何重叠,或者只是按照从上到下的优先级顺序完全冗余的模式.你的基本摇滚乐是一样的.例如,从开始

  xs covering {[], ys}

用[xs:= []]证明其中的第一个,所以分裂.请注意,我们必须使用构造函数case来细化ys以维护不变量.

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

显然,第一种情况严格来说是重叠.另一方面,当我们注意到需要精炼实际程序模式来维护不变量时,我们可以过滤掉那些变得多余的严格改进并检查至少有一个存活(如本::例中的情况).

因此,该算法以由实际程序模式p驱动的方式构建一组理想的穷举重叠模式q.只要实际模式需要特定变量的更多细节,就可以将理想模式拆分为构造函数.如果幸运的话,每个实际模式都由不相交的非空理想模式组覆盖,每个理想模式仅由一个实际模式覆盖.产生理想模式的案例分裂树为您提供了有效的跳转表驱动的实际模式编译.

我提出的算法显然是终止的,但如果有数据类型没有构造函数,它可能无法接受空集模式是穷举的.这在依赖类型语言中是一个严重的问题,传统模式的详尽性是不可判定的:明智的方法是允许"反驳"以及方程式.在Agda中,你可以在任何不能进行构造函数优化的地方写(),发音为"我的阿姨范妮",并且这使得你无需用返回值来完成方程.通过添加足够的反驳,可以使每个详尽的模式集合可识别.

无论如何,这是基本的图片.