Could GHC consider having a warning for the guard-case like it does with the pattern-match itself?
Consider the following:
data X = A Int
h :: X -> Bool
h (A x) = True
h (A x) = False -- Warning! Redundant pattern match
f :: X -> Bool
f (A x)
| x < 50 = True
| otherwise = False
g :: X -> Bool
g (A x) | x < 50 = True
g (A x) = False -- Could be a warning! Duplicated pattern match with guard
g' :: X -> Bool
g' (A x) | x < 50 = True
g' (A x) | x < 50 = False -- Could be be a warning! Duplicated pattern match with guard
h is a warning at present. f is fine. The other two are not even noticed by the compiler as potentially problematic. Could they also be warnings? Or do people consider this a feature?
Are you specifically interested in the case where there is a pattern match? I donāt see why that is relevant. How do you feel about a similar situation without a pattern match:
g :: Int -> Bool
g x | x < 50 = True
g x = False
Do you not want a warning there? If not, what makes the situation different?
You are right; Iām less interested in the pattern match, more upset about the problem of g'; that should clearly be a warning. And If g' is a warning g may as well be a warning too.
I.e. in your example Iād be happy for a warning there as well.
@ozkutuk indeed thereās nothing āwrongā with g; maybe people consider it a feature; itās why I ask. But I encountered it in a codebase and normally, when I see pattern matches, I assume each case is different, but here it wasnāt, it was just a different way to specify the otherwise clause; which I personally found confusing.
The way it is currently implemented in GHC, otherwise is literally defined as True, so every pattern group that include otherwise has overlapping guards in that regard. Thatās also why itās necessary to put the otherwise branch as the very last definition. At the very least, I expect otherwise needs to be treated as a special keyword in order to provide a warning like you suggest, so that it doesnāt warn on otherwise usage.
I donāt see what the implementation of otherwise has to do with it, really.
That could be dropped entirely; itās just the idea that you can specify a series of conditional statements on the roughly the same data in totally different places.
If I am not mistaken, the two patterns are very different things inside GHC and only share a syntactic similarity. Since GHC.Hs.Pat does not mention guards, I guess pattern guards are desugared to view patterns. After all, the condition could be an arbitrary expression in x that evaluates to Bool. Can some GHC dev confirm this?
Would you also consider these two duplicated pattern matches worth a warning?
g'' (A x) | x < 50 = True
g'' (A x) | x >= 40 = False
Should there be no warning when the second number is 50 instead of 40?
Making it a warning could be a pretty difficult task. Since thereās no limit to what you can put in a guard (well, it has to evaluate to a boolean, but thatās it), this would require analysing all existing patterns to see if they are covering everything and not overlapping. That would basically require coq to be embedded into GHC. Then thereās the case of intentional overlap, with otherwise and missing guard being most obvious examples, but in general any special-casing would do. And then thereās the case of intentional not-completeness, e.g. when we guard on length of list and the type system wonāt tell us that the list is limited to no longer than 5 elements (Iād agree this would be a code smell though).
I donāt think@silky is talking about analyzing the content of guards for redundancy. It seems like theyāre saying that, because you can always rewrite
f (some pattern) | a guard = foo
f (some pattern) | another guard (or none) = bar
as
f (some pattern) | a guard = foo
| another guard (or āotherwiseā) = bar
, that the latter should be preferred and the former should be a warning. Is that right?
I agree itās a good point @Torinthiel and @olf that there is trouble if you dive into evaluating the conditions; thatās fine (maybe I shouldāve left that point out), I just want a warning on the mildily confusing siutation of separately defining guards on the same pattern.
This hints at an algebra of patterns, with a possible normal form and the possibility of warning that patterns are not in normal form. Am I right that currently no such algebraic structure exists on Pat or MatchGroup?
Patterns select a subset of a type (and can bind those elements to local variables). Hence as a first approximation, every pattern on a type T can be mapped to a predicate T -> Bool. Here we have the structure of a Boolean algebra. For example,
the WildPat pattern maps to the predicate const True
the Just _ pattern corresponds to the predicate isJust.
We can then ask: What elements of the type T can be distinguished by patterns? If we include view patterns, then the answer is all elements, but for more well-behaved pattern classes the algebra is coarser. Think about function types: What non-trivial patterns are there on a -> b that are not guarded or view patterns? The key insight is then that the quotient of T containing the equivalence classes of pattern-indistinguishable elements often is morally finite and static analysis is possible.
It might not just be distinguishability at play here. One question comes to mind: given the premise of the thread, should this be a warning?
f (_, x) | x > 5 = x + 1
f (x, _) = x - 1
Both patterns accept the same set of pairs (all of them, modulo concerns about bottom), and you can rewrite this to use only one pattern with two guards:
f (x, y) | y > 5 = y + 1
| otherwise = x - 1
But you have to rename a variable to do it. If this is a warning, it might ruffle some feathers. If it isnāt a warning, then the āalgebra of patternsā approach doesnāt look like a Boolean algebra anymore; thereās some important extra structure corresponding to the names that the pattern introduces.
Yes, the variable binding is brushed under the carpet in my Boolean algebra description. Yet it is not inconceivable that the hypothetical pattern algebra has the power to (internally) rename local variables, like any implementation of lambda calculus has.