How to deal with non-exhaustive pattern matching?

Question

I'm giving my function a list as a parameter but I know that it can ever be either empty list or list with one single element.

When I do pattern matching I get a warning about non-exhaustive patterns. I can ignore it and the code works but what are some idiomatic ways of doing this?

Answer 1

There are several techniques. (Some untested code follows.)

Restricting the domain

Instead of

useList :: [a] -> T

we can use a type for non-empty-lists:

useList :: NonEmptyList a -> T

Willem's answer already explains this.

Weakening the codomain

We can instead use

useList :: [a] -> Maybe T
useList (x:xs) = Just (...) -- as before
useList []     = Nothing

and make the pattern matching to be exhaustive. This is however less convenient for the caller who has to handle the Nothing case, which we might know to never happen.

Partial, but documented function

We can instead error out:

useList :: [a] -> T
useList (x:xs) = (...) -- as before
useList []     = error "useList: empty list"

This also makes the pattern matching to be exhaustive. It suppresses the warning, at the cost of producing a runtime error message, which we can customize.

In some cases, there is no pragmatic better alternative. For instance, assume we are using an algorithm to solve a complex task, and said algorithm keeps (or at least, should keep) an invariant where the list is always non empty. Then, instead of

useList :: [a] -> Int
useList (x:xs) = (...)
useList []     = -1          -- it never happens, so we can return anything

it is better to use

useList :: [a] -> Int
useList (x:xs) = (...)
useList []     = "useList: internal error -- non null list invariant broken!"

The latter makes it possible to detect a bug as early as possible.

GADTs proofs

Sometimes we can pass information using GADTs which help to make pattern matching exhaustive. For instance, one could use a type for tagged lists, where the tag represents the emptiness

data Tag = Empty | NonEmpty

data List (t :: Tag) a where
   Nil  :: List 'Empty a
   Cons :: a -> List t a -> List 'NonEmpty a

Then,

useList :: List 'NonEmpty a -> T
useList (Cons x xs) = ...

is exhaustive, even if we never handle the Nil case.

GHC also allows the "non emptiness proof" to be passed separately:

data IsNonEmpty (t :: Tag) where
   IsNE :: IsNonEmpty 'NonEmpty

useList :: IsNonEmpty t -> List t a -> T
useList IsNE (Cons x xs) = ...

is also considered to be exhaustive.

Answer 2

You can make a function where you make it "impossible" to pass such list. Indeed you can implement a function:

atLeastTwo :: a -> a -> [a] -> b

So here the first two parameters represent the first and the second element, and the third parameter, the list, contains the remaining elements. You thus can implement a function, where the check if a function is exhaustive is useful, since you check that for the last parameter (the elements after the first two elements), all patterns are covered.

or we can work with NonEmpty to represent a non-empty list:

atLeastTwo :: a -> NonEmpty a -> b

NonEmpty is defined as:

data NonEmpty = a :| [a]

It is thus a type with one data constructor, that forces that the "list" contains at least one element.