2

Consider a function disjoint :: (Eq a, Ord a) => [a] -> [a] -> Bool which checks if there exists a common element between two sorted lists (and if it does, it returns False since they wouldn't be disjointed).

disjoint :: (Eq a, Ord a) => [a] -> [a] -> Bool
disjoint [] _ = True
disjoint _ [] = True
disjoint (x:xs) (y:ys)
  | x == y = False
  | x < y = disjoint xs (y:ys)
  | x > y = disjoint (x:xs) ys

In my IDE vscode, it yields the following warning:

Pattern match(es) are non-exhaustive
In an equation for ‘disjoint’: Patterns not matched: (_:_) (_:_)compile(-Wincomplete-patterns)

Writing it in a different yet similar way, by using the otherwise clause, will yield no errors:

disjoint :: (Eq a, Ord a) => [a] -> [a] -> Bool
disjoint [] _ = True
disjoint _ [] = True
disjoint (x:xs) (y:ys)
  | x < y = disjoint xs (y:ys)
  | x > y = disjoint (x:xs) ys
  | otherwise = False

What "pattern" does the first code block "miss"? In other words, at what parameters will the first block of code have problems with?

janreggie
  • 334
  • 1
  • 4
  • 12
  • 1
    It does not know that if `x < y` does not hold, and `x > y` does not hold, that `x == y` will always hold. – Willem Van Onsem Jul 07 '21 at 12:36
  • So it is possible for two values of type `Eq a, Ord a` where none of the three relations hold? Could you provide an example? – janreggie Jul 07 '21 at 12:54
  • 4
    @janreggie You can define a custom (bogus) instance for a user-defined type where all the comparisons are always false. Also, NaN in floating point arithmetic have this nasty behavior. – chi Jul 07 '21 at 12:57
  • I'm testing it right now and you're right. Thanks! – janreggie Jul 07 '21 at 13:11
  • 1
    Keep in mind that, when checking exhaustiveness, GHC ignores a guarded equation like `foo Pattern | condition1 = .... | condition2 = ...` unless the very last guard is `otherwise` or `True`. In all the other cases, GHC is conservative and assumes there are cases that fall through all the guards (even if the guards are indeed exhaustive like `f x | ()==() = "hi"`). A semi-rationale is: if you know they are exhaustive, you should "optimize" your code anyway, replacing the last guard with `otherwise` which is faster than any actual test. – chi Jul 07 '21 at 17:33

2 Answers2

7

Eq is a superclass of Ord so you can omit it from the constraint.

You can use compare to turn it into data Ordering = LT | EQ | GT which only has three cases, allowing the compiler to infer exhaustiveness.

disjoint :: Ord a => [a] -> [a] -> Bool
disjoint [] _ = True
disjoint _ [] = True
disjoint (x:xs) (y:ys) =
  case x `compare` y of
    EQ -> False
    LT -> disjoint xs (y:ys)
    GT -> disjoint (x:xs) ys
Iceland_jack
  • 6,848
  • 7
  • 37
  • 46
3

From @chi's comment here:

Consider the following data type:

data TT = Bogus 
instance Eq TT where
  Bogus == Bogus = False
instance Ord TT where
  Bogus <= Bogus = False
  Bogus < Bogus = False
  Bogus >= Bogus = False
  Bogus > Bogus = False

Any comparisons between a Bogus and a Bogus returns False. Because of that,

> disjoint [Bogus, Bogus] [Bogus, Bogus]
*** Exception: Ch04Book.hs:(25,1)-(30,18): Non-exhaustive patterns in function disjoint

The same Exception is raised when running disjoint [acos 2] [acos 2] since comparisons between NaNs always returns False.

Sidenote/implication: A type of typeclass Ord does not necessarily follow the Law of excluded middle. See Bogus where both Bogus < Bogus = False and Bogus >= Bogus = False, and Haskell would not complain.

janreggie
  • 334
  • 1
  • 4
  • 12
  • 1
    I wouldn't really call it bogus; `Ord` isn't required to implement a total order, so it's perfectly legal for distinct objects to be noncomparable. – chepner Jul 07 '21 at 15:35
  • 1
    @chepner What about `compare`, though? If it's not a total order, we have to make that crash (or fail to terminate). If `Ord` is not supposed to model a total order, it should not have a `compare` method, IMO. For the record, `compare (acos 2) (acos 2)` returns `GT` here. – chi Jul 07 '21 at 17:23
  • The exhaustiveness checker does not know about the laws of *any* typeclasses. Even if `Ord` had some law which says that `==`, `<`, and `>` are exhaustive (disjoint), the compiler would give the same exact warning for the code in the OP. While all the statements in this answer are essentially true, they do not answer the question. – user2407038 Jul 07 '21 at 17:38