Nat3.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}


-- Naturals.

data Nat :: * where
  Zero :: Nat
  Suc  :: Nat -> Nat

instance Eq Nat where
  Zero  == Zero   = True
  Suc n == Suc n' = n == n'
  _     == _      = False

instance Ord Nat where
  Zero  <= _      = True
  Suc n <= Suc n' = n <= n'
  _     <= _      = False

instance Enum Nat where
  fromEnum Zero        = 0
  fromEnum (Suc n)     = fromEnum n + 1
  toEnum n | n == 0    = Zero
           | n > 0     = Suc (toEnum (n - 1))
           | otherwise = error "Cannot cast negative Int to Nat"

instance Show Nat where
  show = show . fromEnum


-- Singletons for naturals.

data SingNat :: Nat -> * where
  SingZero :: SingNat Zero
  SingSuc  :: forall n. SingNat n -> SingNat (Suc n)
  
class IsNat (n :: Nat) where
  singNat :: SingNat n
  
instance IsNat Zero where
  singNat = SingZero
  
instance IsNat n => IsNat (Suc n) where
  singNat = SingSuc singNat