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

Question

如何确定一个给定的模式是否“好”，即它是否是穷尽和非重叠的，适用于 ML 风格的编程语言？

假设你有以下类型的模式：

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

或者：

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

一个好的类型检查器会警告第一个不是穷尽的，而第二个是重叠的。通常情况下，类型检查器将如何对任意数据类型做出这些决策？

- Tommy McGuire

---

模式匹配展开通常在类型推断之后单独进行处理。 - SK-logic

Answer 1

这是一个算法的草图。它也是Lennart Augustsson编译模式匹配高效的著名技术的基础。（这篇论文发表在那个令人难以置信的FPCA会议论文集（LNCS 201），有很多引用。）这个想法是通过反复将最一般的模式分解为构造器情况，重建一个详尽且非冗余的分析。

一般来说，问题是你的程序可能有一堆可能为空的“实际”模式{p₁，..，p_n}，而你想知道它们是否覆盖了给定的“理想”模式q。为了开始，将q设为一个变量x。不变量最初被满足，并随后保持不变的是，每个p_i都是σ_iq，其中σ_i是将变量映射到模式的替换。

如何进行。如果n=0，那么这个集合是空的，所以你有一个可能的情况q没有被一个模式覆盖。抱怨ps不是穷尽的。如果σ₁是一个变量的可逆重命名，那么p₁会捕捉到与q匹配的每种情况，所以我们很接近成功：如果n=1，我们就赢了；如果n>1，那么糟糕了，p₂永远不会被需要。否则，对于某个变量x，σ₁x是一个构造模式。在这种情况下，将问题分解为多个子问题，每个子问题对应x的类型的每个构造函数c_j。也就是说，将原始的q分解为多个理想模式q_j = [x:=c_j y₁ .. y_arity(cj)]q，并根据每个q_j相应地细化模式，以保持不变性，丢弃那些不匹配的模式。

让我们以{[], x :: y :: zs}的例子开始。我们从这里开始。

  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 := []]` 来证明第一个，所以进行拆分。请注意，我们必须使用构造器来细化 `ys` 以保持不变性。

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

显然，第一个情况严格来说是一个重叠。另一方面，当我们注意到需要改进实际程序模式以保持不变性时，我们可以过滤掉那些变得多余的严格改进，并检查至少有一个改进保留下来（就像这里的::情况一样）。

因此，该算法通过一种受实际程序模式p启发的方式构建了一组理想的穷尽重叠模式q。当实际模式要求更多特定变量的详细信息时，您将理想模式分割为构造器情况。如果幸运的话，每个实际模式都由不相交的非空理想模式集合覆盖，并且每个理想模式只被一个实际模式覆盖。产生理想模式的情况分割树为您提供了实际模式的高效跳转表驱动编译。

我提出的算法显然是终止的，但如果存在没有构造函数的数据类型，它可能无法接受空模式集是穷尽的事实。这在依赖类型语言中是一个严重的问题，因为常规模式的穷尽性是不可判定的：明智的做法是允许“反驳”以及等式。在Agda中，你可以在任何无法进行构造函数细化的地方写上“()”，发音为“my Aunt Fanny”，这样就不需要在等式中补全返回值了。通过添加足够的反驳，可以使每个穷尽的模式集变得“可识别”穷尽。

总之，这就是基本情况。

- pigworker

---

我不确定'banjaxed'是什么意思，但听起来不太好。我确实看到了Lennart Augustsson的'Compiling pattern matching'的参考资料，但我还没有找到一份副本。谢谢你的回答！ - Tommy McGuire

粗略地说，“banjaxed”意味着“困惑”或“无法修复”。这是一个爱尔兰的说法。同时，Lennart的论文在http://www.springerlink.com/content/y647423656557505/上被封锁了。我不知道是否有更便宜的选择。 - pigworker

我不明白你的阿姨与这整个模式匹配业务有什么关系 :) - didierc

Answer 2

这里有一些来自非专家的代码。它展示了如果你限制你的模式为列表构造函数会看起来怎样。换句话说，这些模式只能用于包含列表的列表。以下是一些类似的列表：[]、[[]]、[[];[]]。

如果你在OCaml解释器中启用了-rectypes，那么这组列表将具有单个类型：('a list) as 'a.

type reclist = ('a list) as 'a

这里有一个类型用于表示与 reclist 类型匹配的模式：

type p = Nil | Any | Cons of p * p

要将OCaml模式转换为这种形式，首先要使用(::)重写它。然后将[]替换为Nil，_替换为Any，(::)替换为Cons。所以模式[] :: _可以翻译为Cons (Nil, Any)。

下面是一个将模式与reclist匹配的函数：

let rec pmatch (p: p) (l: reclist) =
    match p, l with
    | Any, _ -> true
    | Nil, [] -> true
    | Cons (p', q'), h :: t -> pmatch p' h && pmatch q' t
    | _ -> false

以下是使用示例。请注意，使用了-rectypes：

$ ocaml312 -rectypes
        Objective Caml version 3.12.0

# #use "pat.ml";;
type p = Nil | Any | Cons of p * p
type reclist = 'a list as 'a
val pmatch : p -> reclist -> bool = <fun>
# pmatch (Cons(Any, Nil)) [];;
- : bool = false
# pmatch (Cons(Any, Nil)) [[]];;
- : bool = true
# pmatch (Cons(Any, Nil)) [[]; []];;
- : bool = false
# pmatch (Cons (Any, Nil)) [ [[]; []] ];;
- : bool = true
# 

模式Cons（Any，Nil）应匹配任何长度为1的列表，并且它似乎确实有效。

因此，编写一个函数intersect似乎非常简单，该函数接受两个模式并返回匹配两个模式的交集的模式。由于这些模式可能根本不相交，当没有交集时它返回None，否则返回Some p。

let rec inter_exc pa pb =
    match pa, pb with
    | Nil, Nil -> Nil
    | Cons (a, b), Cons (c, d) -> Cons (inter_exc a c, inter_exc b d)
    | Any, b -> b
    | a, Any -> a
    | _ -> raise Not_found

let intersect pa pb =
    try Some (inter_exc pa pb) with Not_found -> None

let intersectn ps =
    (* Intersect a list of patterns.
     *)
    match ps with
    | [] -> None
    | head :: tail ->
        List.fold_left
            (fun a b -> match a with None -> None | Some x -> intersect x b)
            (Some head) tail

作为一个简单的测试，将模式[_, []]与模式[[], _]相交。 前者与_ :: [] :: []相同，因此是Cons（Any，Cons（Nil，Nil））。 后者与[] :: _ :: []相同，因此是Cons（Nil，（Cons（Any，Nil））。

# intersect (Cons (Any, Cons (Nil, Nil))) (Cons (Nil, Cons (Any, Nil)));;
- : p option = Some (Cons (Nil, Cons (Nil, Nil)))

结果看起来很正确：[[], []]。

如果两个模式的交集不是None，它们就重叠了。

为了全面性，您需要处理一个模式列表。下面是一个名为exhaust的函数，用于测试给定的模式列表是否全面：

let twoparts l =
    (* All ways of partitioning l into two sets.
     *)
    List.fold_left
        (fun accum x ->
            let absent = List.map (fun (a, b) -> (a, x :: b)) accum
            in
                List.fold_left (fun accum (a, b) -> (x :: a, b) :: accum)
                    absent accum)
        [([], [])] l

let unique l =
   (* Eliminate duplicates from the list.  Makes things
    * faster.
    *)
   let rec u sl=
        match sl with
        | [] -> []
        | [_] -> sl
        | h1 :: ((h2 :: _) as tail) ->
            if h1 = h2 then u tail else h1 :: u tail
    in
        u (List.sort compare l)

let mkpairs ps =
    List.fold_right
        (fun p a -> match p with Cons (x, y) -> (x, y) :: a | _ -> a) ps []

let rec submatches pairs =
    (* For each matchable subset of fsts, return a list of the
     * associated snds.  A matchable subset has a non-empty
     * intersection, and the intersection is not covered by the rest of
     * the patterns.  I.e., there is at least one thing that matches the
     * intersection without matching any of the other patterns.
     *)
    let noncovint (prs, rest) =
        let prs_firsts = List.map fst prs in
        let rest_firsts = unique (List.map fst rest) in
        match intersectn prs_firsts with
        | None -> false
        | Some i -> not (cover i rest_firsts)
    in let pairparts = List.filter noncovint (twoparts pairs)
    in
        unique (List.map (fun (a, b) -> List.map snd a) pairparts)

and cover_pairs basepr pairs =
    cover (fst basepr) (unique (List.map fst pairs)) &&
        List.for_all (cover (snd basepr)) (submatches pairs)

and cover_cons basepr ps =
    let pairs = mkpairs ps
    in let revpair (a, b) = (b, a)
    in
        pairs <> [] &&
        cover_pairs basepr pairs &&
        cover_pairs (revpair basepr) (List.map revpair pairs)

and cover basep ps =
    List.mem Any ps ||
        match basep with
        | Nil -> List.mem Nil ps
        | Any -> List.mem Nil ps && cover_cons (Any, Any) ps
        | Cons (a, b) -> cover_cons (a, b) ps

let exhaust ps =
    cover Any ps

一个模式就像是一个树，内部节点有Cons，在叶子节点上有Nil或Any。基本思想是，如果一组模式总是在至少一个模式中达到Any（无论输入长什么样），则该组模式是穷尽的。在这个过程中，您需要在每个点上看到Nil和Cons。如果在所有模式的相同位置上达到Nil，则意味着存在一组更长的输入，它们都不能匹配。另一方面，如果在所有模式的相同位置上只有Cons，则意味着存在一个在该点结束的输入，它将不会被匹配。

难点在于检查Cons的两个子模式是否穷尽。这段代码的工作方式就像我手动检查时那样：它找到了可能匹配左侧的所有不同子集，然后确保在每种情况下对应的右侧子模式都是穷尽的。然后再通过左右翻转进行相同的操作。由于我是一个非专家（越来越明显了），所以可能有更好的方法来实现这一点。

以下是使用此函数的会话：

# exhaust [Nil];;
- : bool = false
# exhaust [Any];;
- : bool = true
# exhaust [Nil; Cons (Nil, Any); Cons (Any, Nil)];;
- : bool = false
# exhaust [Nil; Cons (Any, Any)];;
- : bool = true
# exhaust [Nil; Cons (Any, Nil); Cons (Any, (Cons (Any, Any)))];;
- : bool = true

我对这段代码进行了30,000个随机生成的模式的测试，因此我相信它是正确的。希望这些谦虚的观察结果能够对你有所帮助。

- Jeffrey Scofield

Answer 3

我相信模式子语言足够简单，易于分析。这就是要求模式“线性”（每个变量只能出现一次）等的原因。在这些限制下，每个模式都是从一种嵌套元组空间到一组受限元组的投影。我认为在这个模型中检查穷举和重叠并不太困难。

- Jeffrey Scofield

---

我能理解线性需求是如何实现的，但我不知道如何做到。 - Tommy McGuire

可以。如何检查是否穷尽和是否存在重叠部分？ - luqui

可能是一个公正的抱怨。我认为将模式设计为在可能性空间中相当简单的切片是有用的。进行高效匹配是一个更难的问题。但是很抱歉没有更多的帮助。与此同时，似乎pigworker给出了一个很好的答案。 - Jeffrey Scofield

以下是关于编程的内容，请将其从英语翻译成中文。只返回翻译后的文本：（我添加了第二个答案，为问题的简化版本提供了可行的代码。--J） - Jeffrey Scofield