nicodelpiano / stlcnat-exhaustivity-checker Goto Github PK

Eventually, we'll want to put this on Hackage, so let's start by packaging it up as a Cabal project. Later we can add it as a dependency in purescript.

• A library with the Match class and its instances and functions
• A separate test suite combining QuickCheck and unit tests (maybe with test-framework?)
• Haddocks for documentation

I think we can write it like this:

instance Match Binder where
  missed _ NullBinder = []

  missed NullBinder b = go b
    where 
    go Zero = [Succ NullBinder]
    go (Succ n) = Zero : map Succ (go n)

  missed Zero Zero = []
  missed (Succ n) (Succ m) = map Succ (missed n m)

  missed b _ = [b]

That is, we have four groups of cases:

• NullBinder matches everything
• If we start with NullBinder, we take the complement of the pattern
• If the patterns match exactly, we return [] (this bit looks like unification)
• Everything else fails to match - return the argument.

This should hopefully make it easier to generalize to other types of pattern.

Could you QuickCheck this to make sure it returns the same results?

For simplicity, we can just require that a pattern with guards has a fallback guard using otherwise.

A type class makes the structure very clear in my opinion:

class Match c where
  missed :: c -> c -> [c]

instance Match Binder where
  missed Zero Zero = []
  missed _ NullBinder = []
  missed NullBinder b =
    let all_pat = [Zero, Succ NullBinder]
    in concat $ map (\cp -> missed cp b) all_pat
  missed (Succ n) (Succ m) =
    let ucs = missed n m
    in (zip_con Succ) ucs
    where
      zip_con :: (Binder -> Binder) -> Case -> Case
      zip_con _ [] = []
      zip_con b bs = (b hps):rest
        where
        (hps, rest) = (head bs, tail bs)
  missed b _ = [b]

(instance copied from your code)

Here's the neat bit. If you define a type of length-indexed lists:

{-# LANGUAGE GADTs, DataKinds #-}

data Nat = Z | S Nat

data Vec n a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

vecToList :: Vec n a -> [a]
vecToList Nil = []
vecToList (Cons x xs) = x : vecToList xs

instance (Show a) => Show (Vec n a) where
  show Nil = "Nil"
  show (Cons x xs) = "(Cons " ++ show x ++ " " ++ show xs ++ ")"

then you can define an instance

instance (Match c) => Match (Vec n c)

Once this instance is implemented, we have proved that the number of arguments matched by the output is the same as the number matched by the input! This is a very important invariant.