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几乎就会考虑模式重叠.

确定函数是否具有重叠模式的正确方法是什么？

---

更新

我正在寻找overlapping patternfp101x课程中使用的定义.

根据fp101x中使用的定义,以下函数具有overlapping patterns:

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

这与GHC定义相矛盾,GHC定义overlapping pattern不认为它具有任何重叠模式.

如果没有正确定义overlapping patternfp101x课程背景中的含义,就无法解决这个问题.那里使用的定义不是GHC的定义.

Answer 1

更新后的问题澄清了OP想要重叠模式的正式定义。这里的“重叠”是指 GHC 在发出警告时使用的含义：即，当它检测到某个 case 分支无法访问时，因为它的模式与先前分支尚未处理的任何内容都不匹配。

可能的正式定义确实可以遵循这种直觉。也就是说，对于任何模式，我们可以首先定义与 匹配的p一组值（表示）。（为此，了解涉及的变量的类型很重要--取决于类型环境。）然后，我们可以说在模式序列中[[p]]pp[[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剩下另一种情况。同样，如果您匹配[]，则还剩下另一种_:_情况。粗略地说，当与 constructor 匹配时K，相同类型的所有其他构造函数都会保留。

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

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