6

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

鉴于：

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

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

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

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

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

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

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

4

4 回答 4

2

更新后的问题澄清了 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情况。同样，如果您匹配[]，则还有另一种_:_情况。粗略地说，当与构造函数匹配时K，相同类型的所有其他构造函数都保留。

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

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

于 2014-12-28T21:43:11.910 回答
1

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

“不依赖于匹配顺序的模式称为不相交或不重叠。” （来自“Haskell 编程”Graham Hutton）

所以这个例子是不重叠的

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

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

于 2015-12-15T05:48:33.873 回答
0

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

这就是 GHC 文档必须说的：

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

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

永远无法达到“f”中的最后一个模式匹配，因为第二个模式与其重叠。通常情况下，冗余模式是程序员的错误/错误，因此默认情况下启用此选项。

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

于 2014-12-28T16:05:37.077 回答
0

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

-- 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 [] = []

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

于 2015-12-23T13:24:28.887 回答