Haskell中重叠模式的含义

Question

我目前对 Haskell 中模式重叠的理解是，如果传递给函数的某些参数值可以被多个模式匹配，则认为 2 个模式是重叠的。

给定：

last :: [a] -> a
last [x] = x
last (_ : xs) = last xs

传递参数值 [1] 将匹配第一个模式 [x] 和第二个模式 (_ : xs) - 这意味着即使两个模式都可以匹配，函数也有重叠的模式。

令人困惑的是，尽管模式（根据上述定义）重叠，但 GHC 并未显示任何关于它们重叠的警告。

还原 last 函数中的 2 个模式匹配确实会显示重叠警告：

last :: [a] -> a
last (_ : xs) = last xs
last [x] = x

警告：

src\OverlappingPatterns.hs:6:1: Warning:
    Pattern match(es) are overlapped
    In an equation for `last': last [x] = ...

如果先前的模式无法匹配后来出现的模式，GHC 就好像认为模式重叠。

判断一个函数是否有重叠模式的正确方法是什么？

---

更新

我正在寻找 fp101x 课程中使用的overlapping pattern 定义。

根据fp101x中使用的定义，下面的函数有overlapping patterns：

last :: [a] -> a
last [x] = x
last (_ : xs) = last xs

这与overlapping pattern 的 GHC 定义相矛盾，后者不认为它具有任何重叠模式。

如果没有正确定义 overlapping pattern 在 fp101x 课程上下文中的含义，就不可能解决该练习。而且那里使用的定义不是 GHC 的。

Answer 1

更新后的问题阐明了 OP 希望对重叠模式进行正式定义。这里的“重叠”是指 GHC 在发出警告时使用的含义：也就是说，当它检测到一个 case 分支不可达时，因为它的模式与之前分支尚未处理的任何东西都不匹配。

一个可能的正式定义确实可以遵循这种直觉。也就是说，对于任何模式p，可以首先定义与p 匹配的一组值（表示）[[p]]。 （为此，重要的是要知道p 中涉及的变量的类型——[[p]] 取决于类型环境Gamma。）然后，可以说在模式序列中

q0 q1 ... qn p

模式p 是重叠的，如果[[p]] 作为一个集合包含在[[q0]] union ... union [[qn]] 中。

不过，上面的定义几乎没有用——它不会立即导致检查重叠的算法。实际上，计算[[p]] 是不可行的，因为它通常是一个无限集。

要定义一个算法，我会尝试为任何模式q0 .. qn 的“尚未匹配”的术语集定义一个表示。例如，假设我们使用布尔列表：

Remaining: _   (that is, any list)

q0 = []
Remaining: _:_  (any non empty list)

q1 = (True:xs)
Remaining: False:_

p = (True:False:ys)
Remaining: False:_

这里，“剩余”集没有改变，所以最后一个模式是重叠的。

再举一个例子：

Remaining: _

q0 = True:[]
Remaining: [] , False:_ , True:_:_

q1 = False:xs
Remaining: [], True:_:_

q2 = True:False:xs
Remaining: [], True:True:_

q3 = []
Remaining: True:True:_

p = True:xs
Remaining: nothing  -- not overlapping (and exhaustive as well!)

如您所见，在每一步中，我们都会将每个“剩余”样本与手头的模式进行匹配。这会生成一组新的剩余样本（可能没有）。所有这些样本的集合形成了新的剩余集合。

为此，请注意了解每种类型的构造函数列表很重要。这是因为在匹配True 时，您必须知道还有另一个False 案例剩余。同样，如果您匹配[]，则还剩下另一个_:_ 案例。粗略地说，当与构造函数K 匹配时，所有其他相同类型的构造函数都会保留。

以上示例还不是算法，但希望它们可以帮助您入门。

当然，所有这些都忽略了大小写保护（这使得重叠无法确定）、模式保护、GADT（可以以非常微妙的方式进一步细化剩余的集合）。

Answer 2

我正在寻找 fp101x 课程中使用的重叠模式定义。

"不依赖于匹配顺序的模式是 称为不相交或不重叠。”（来自“Haskell 编程”） 格雷厄姆·赫顿）

所以这个例子不会重叠

foldr :: (a → b → b) → b → [a] → b
foldr v [] = v
foldr f v (x : xs) = f x (foldr f v xs)

因为您可以像这样更改模式匹配的顺序：

foldr :: (a → b → b) → b → [a] → b
foldr f v (x : xs) = f x (foldr f v xs)
foldr v [] = v

在这里你不能：

last :: [a] -> a
last [x] = x
last (_ : xs) = last xs

所以最后一个 )) 是重叠的。

Answer 3

我认为问题在于，在第一种情况下，并非所有 [x] 的匹配项都会匹配 (_:xs)。在第二种情况下，反之亦然（没有一个匹配的 (_:xs) 会落入 [x]）。因此，重叠确实意味着存在无法到达的模式。

这就是 GHC 文档必须说的：

默认情况下，如果有一组模式，编译器会警告你 不完整（即，您只匹配代数的子集 数据类型的构造函数），或重叠，即，

f :: String -> Int
f []     = 0 
f (_:xs) = 1 
f "2"    = 2

永远不会到达 `f' 中的最后一个模式匹配，因为 第二个图案与它重叠。很多时候，多余的 模式是程序员的错误/错误，所以这个选项被启用 默认。

也许“无法到达的模式”是一个更好的词选择。

Answer 4

我建议将推理逻辑与编译器消息和测试结果结合使用，这将是了解函数是否具有重叠模式的更好方法。作为两个示例，第一个已经列出，确实会导致编译器警告。

-- The first definition should work as expected.
last1 :: [a] -> a
last1 [x] = x
last1 (_:xs) = last xs

在第二种情况下，如果我们交换最后两行，则会出现编译器错误。 程序错误：模式匹配失败：init1 [] 结果

last :: [a] -> a
last (_:xs) = last xs
last [x] = x

这与传递可以匹配两种模式的单例列表的逻辑相匹配，在这种情况下是现在的第二行。

last (_:xs) = last xs

在这两种情况下都会匹配。如果我们接着进入第二个例子

-- The first definition should work as expected
drop :: Int -> [a] -> [a]
drop 0 xs = xs
drop n [] = []
drop n (_:xs) = drop1 (n - 1) xs

在第二种情况下，如果我们再次将最后一行与第一行交换，那么我们不会得到编译器错误，但也不会得到我们期望的结果。 Main> drop 1 [1,2,3] 返回一个空列表[]

drop :: Int -> [a] -> [a]
drop n (_:xs) = drop1 (n - 1) xs
drop 0 xs = xs
drop n [] = []

总之，我认为这就是为什么确定重叠模式的推理（与正式定义相反）可以正常工作的原因。