Nat.purs

-- The Nat type class is to be seen as a port of the Nat type to the type level.
--
-- At value level, the usual Nat type only posseses two constructors by being defined as followed:
--
-- data Nat = Z | S Nat
--
-- Being then usable by pattern matching on the constructor as following:
-- 
-- foo :: Nat -> ...
-- foo n = case n of
--      Z    -> ...
--      S n' -> ...
--
-- To make the Nat type class usable as the usual Nat type, we provide the `split` function, implementing
-- pattern matching on the type level Nat. Pattern matching at the type level, like at the value level,
-- should inform the user about which constructor was used to instantiate the type, here which type has used
-- to instantiate the type class, and with which parameters.
--
-- At the type level, we translate the value level pattern matching as followed:
--
-- foo :: forall n. Nat n => ...
-- foo = case split of
--    Left  (p :: n ~ Z)     -> ...
--    Right (p :: HasPred n) -> ...
-- 
-- Which provides us a proof that n is Z (p :: n ~ Z) or a proof that n was constructed as the successor of
-- another Nat, which is encoded using the HasPred type alias, which represents the proof of
-- ∃n': Nat n' => n ~ S n', which is the same as what we had at type level with the usual Nats.
class Nat n where
  split :: (n ~ Z) \/ (HasPred n)
  
data Z
instance zeroNat :: Nat Z where
  split = Left refl

data S n
instance succNat :: Nat n => Nat (S n) where
  split = Right (mkExistsNat $ Comp refl)