Skip to content

Instantly share code, notes, and snippets.

@mrBliss

mrBliss/SNat.hs

Created September 24, 2019 10:05
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mrBliss/981b377200ba14c9c65fbb53b770dd84 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mrBliss/981b377200ba14c9c65fbb53b770dd84 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
-}
@kosmikus
Copy link

kosmikus commented Sep 24, 2019 

{-# 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment