Haskell Overlapping Pattern Value

Question

My current understanding of pattern overlapping in Haskell is that 2 patterns are considered overlapping if some of the argument values ​​passed to the function can be matched by multiple patterns.

Given:

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

passing the value of argument [1] will correspond to both the first pattern [x] and the second pattern (_: xs) - so this means that the function has overlapping patterns, even if both patterns can be matched.

What is confusing is that although the patterns (as defined above) overlap, the GHC does not show any warnings that they overlap.

Returning two pattern matches in the last function shows an overlap warning:

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

Attention:

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

It is very likely that the GHC considers overlapping patterns if the previous pattern does not allow matching the pattern that occurs later.

What is the correct way to determine if a function has overlapping patterns or not?

---

Update

I am looking for the definition of overlapping pattern used in the fp101x course.

According to the definition used in fp101x, the following function has overlapping patterns :

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

This contradicts the GHC overlapping pattern definition, which does not consider that it has any overlapping patterns.

Without correctly defining what the overlapping pattern means in the context of the fp101x course, it is impossible to solve this exercise. And the definition used there is not a GHC.

Answer 1

The updated question clarifies that the OP wants a formalized definition of overlapping patterns. Here, “overlap” is implied in the sense that the GHC uses when it issues its warnings: that is, when it detects that the case branch is unreachable because its template does not match with anything that is not being processed by the previous branch.

A possible formal definition may indeed follow this intuition. That is, for any pattern p , you can first define a set of values ​​(notation) [[p]] corresponding to p . (For this, it is important to know the type of variables involved in p - [[p]] , it depends on the environment of the Gamma type.) Then we can say that in the sequence of patterns

 q0 q1 ... qn p 

the pattern p overlaps if if [[p]] , as a set, is included in [[q0]] union ... union [[qn]] .

The above definition is unlikely to apply, although it does not immediately lead to an overlap verification algorithm. Indeed, the calculation of [[p]] impossible, since it is an infinite set in general.

To define an algorithm, I would try to define a representation for a set of terms “not yet consistent” with any q0 .. qn pattern. As an example, suppose we are working with logical lists:

 Remaining: _ (that is, any list) q0 = [] Remaining: _:_ (any non empty list) q1 = (True:xs) Remaining: False:_ p = (True:False:ys) Remaining: False:_ 

Here the "remaining" set has not changed, so the last template overlaps.

As another example:

 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!) 

As you can see, at each step we compare each of the remaining samples with the sample at hand. This creates a new set of remaining samples (maybe not). A collection of all these patterns forms the new remaining set.

To do this, note that it is important to know the list of constructors for each type. This is because when comparing with True you should know that another case of False remains. Similarly, if you compare with [] , there remains one more case of _:_ . Roughly speaking, when comparing with the constructor K , all other constructors of the same type remain.

The above examples are not an algorithm yet, but hopefully you can start with you.

All this, of course, ignores the protective covers (which make the overlap insoluble), protective masks, GADT (which can further clarify the remaining set in rather subtle ways).

Answer 2

I am looking for the definition of an overlapping pattern used in the fp101x course.

"Patterns that are independent of the order in which they match, called non-overlapping or non-overlapping." (from "Haskell Programming" by Graham Hatton)

So this example will not overlap

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

Since you can change the pattern matching order as follows:

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

And here you cannot:

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

So the last one)) overlaps.

Answer 3

I think the fact is that in the first case, not all matches [x] will match (_: xs). In the second case, the converse is true (no match (_: xs) passes through [x]). So overlapping really means that there is an unreachable pattern.

This is what the GHC documentation has to say about this:

By default, the compiler will warn you if the set of templates is incomplete (i.e. you are only matching on a subset of algebraic data type constructors) or overlapping, i.e.

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

where the last pattern match in `f 'will never be reached since the second pattern overlaps it. Most often redundant templates are a programmer error / error, therefore this option is enabled by default.

Perhaps an “unreachable pattern” would be a better choice of words.

Answer 4

I would suggest using reasoning in conjunction with compiler messages, and test results would be the best way to understand if a function has overlapping patterns or not. As two examples, the first one that has already been specified does lead to a compiler warning.

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

in the second case, if we replace the last two lines around the compiler error. Software error: template failed: init1 [] results

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

This corresponds to the logic of the transmission of a singleton list, which may coincide in both patterns, in which case the second line.

 last (_:xs) = last xs 

will match in both cases. If we move on to the second example

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

In the second case, if we again replace the last line with the first line, we will not get a compiler error, but we also will not get the expected results. Main> drop 1 [1,2,3] returns an empty list []

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

In general, I think that’s why the reasoning (as against the formal definition) for defining overlapping patterns works fine.