Exhaustivity checking using prisms

Main.hs

module Main where

-- We will define our checker by piecing together functions based on the various types of binders.
-- We use prisms to abstract over the data constructors representing binders
type Prism a b = (a -> b, b -> Maybe a)

-- As an example, suppose we want to check array binders [_, _, ..., _] for exhaustivity.
-- We could introduce two constructors ArrNil and ArrCons, and require these constructors be
-- binders in our language.
data Array b = ArrNil | ArrCons b b deriving (Show)

-- Here, I'm just implementing the "complement" function, which generates all
-- patterns uncovered by a given pattern. This function lifts such a function to
-- handle array binders.
missArray :: Prism Wildcard b -> Prism (Array b) b -> (b -> [b]) -> b -> [b]
missArray (wild, _) (inj, prj) f b =
  case prj b of
    Just arr -> go arr
    Nothing -> f b
  where
  go ArrNil = [inj (ArrCons (wild Wildcard) (wild Wildcard))]
  go (ArrCons x xs) = inj ArrNil : map (inj . (`ArrCons` xs)) (f x) ++ map (inj . ArrCons x) (f xs)
    
-- We can handle wildcards similarly
data Wildcard = Wildcard

missWildcard :: Prism Wildcard b -> (b -> [b]) -> b -> [b]
missWildcard (_, prj) f b =
  case prj b of
    Just _ -> []
    Nothing -> f b

-- Now we can assemble our complement function piece-by-piece by specifying a few prisms.                         
data Test = Wild | Arr (Array Test) deriving (Show)

test = missArray wildPrism arrPrism 
     . missWildcard wildPrism
     $ test

arrPrism = (Arr, isArr)
  where 
  isArr (Arr a) = Just a
  isArr _ = Nothing
  
wildPrism = (const Wild, isWild)
  where
  isWild Wild = Just Wildcard
  isWild _ = Nothing