SNat.hs

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns    #-}

-- | Type-level index
data N = Z | S N

-- | Value-level type indexed by type-level index
data Nat (n :: N) where
  Zero ::          Nat Z
  Succ :: Nat n -> Nat (S n)

isZero :: Nat n -> Bool
isZero Zero     = True
isZero (Succ _) = False




-- | Now let's represent 'Nat' using an 'Int': 'SNat'.
newtype SNat (n :: N) = UnsafeInt Int

-- Let's define pattern synonyms so we can still write inductive functions
-- like before.
pattern SZero :: SNat Z
pattern SZero = UnsafeInt 0

pattern SSucc :: SNat n -> SNat (S n)
pattern SSucc n <- (snatPred -> Just n) where
  SSucc (UnsafeInt n) = UnsafeInt (succ n)

snatPred :: SNat (S n) -> Maybe (SNat n)
snatPred (UnsafeInt 0) = Nothing
snatPred (UnsafeInt n) = Just (UnsafeInt (pred n))

{-# COMPLETE SZero, SSucc #-}


-- But this doesn't compile:
isSZero :: SNat n -> Bool
isSZero SZero     = True
isSZero (SSucc n) = False

{-
    • Couldn't match type ‘n’ with ‘'Z’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          isSZero :: forall (n :: N). SNat n -> Bool
      Expected type: SNat n
        Actual type: SNat 'Z
    • In the pattern: SZero
      In an equation for ‘isSZero’: isSZero SZero = True
    • Relevant bindings include
        isSZero :: SNat n -> Bool
-}

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns    #-}

import Unsafe.Coerce

-- | Type-level index
data N = Z | S N

-- | Value-level type indexed by type-level index
data Nat (n :: N) where
  Zero ::          Nat Z
  Succ :: Nat n -> Nat (S n)

isZero :: Nat n -> Bool
isZero Zero     = True
isZero (Succ _) = False

data IsNat (n :: N) where
  IsZero :: IsNat Z
  IsSucc :: SNat n -> IsNat (S n)

toNat :: SNat n -> IsNat n
toNat (UnsafeInt 0) = unsafeCoerce IsZero
toNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n)))

-- | Now let's represent 'Nat' using an 'Int': 'SNat'.
newtype SNat (n :: N) = UnsafeInt Int

-- Let's define pattern synonyms so we can still write inductive functions
-- like before.
pattern SZero :: () => (Z ~ n) => SNat n
pattern SZero <- (toNat -> IsZero)
  where
    SZero = UnsafeInt 0

pattern SSucc :: () => (m ~ S n) => SNat n -> SNat m
pattern SSucc n <- (toNat -> IsSucc n) where
  SSucc (UnsafeInt n) = UnsafeInt (succ n)

{-# COMPLETE SZero, SSucc #-}


-- But this doesn't compile:
isSZero :: SNat n -> Bool
isSZero SZero     = True
isSZero (SSucc n) = False