GHC/TypeLits.hs (original) (raw)

module GHC.TypeLits ( Nat, Symbol

, Sing, SingI, SingE, SingRep, sing, fromSing , unsafeSingNat, unsafeSingSymbol , Kind

, withSing, singThat

, type (<=), type (<=?), type (+), type (*), type (^)

, isZero, IsZero(..) , isEven, IsEven(..) ) where

import GHC.Base(Eq((==)), Bool(..), ($), otherwise, (.)) import GHC.Num(Integer, ()) import GHC.Base(String) import GHC.Read(Read(..)) import GHC.Show(Show(..)) import GHC.Prim(Any) import Unsafe.Coerce(unsafeCoerce) import Data.Bits(testBit,shiftR) import Data.Maybe(Maybe(..)) import Data.List((++))

type Kind = Any

data Nat

data Symbol

data family Sing (n :: k)

newtype instance Sing (n :: Nat) = SNat Integer

newtype instance Sing (n :: Symbol) = SSym String

unsafeSingNat :: Integer -> Sing (n :: Nat) unsafeSingNat = SNat

unsafeSingSymbol :: String -> Sing (n :: Symbol) unsafeSingSymbol = SSym

class SingI a where

sing :: Sing a

class (m :: Nat) <= (n :: Nat)

type family (m :: Nat) <=? (n :: Nat) :: Bool

type family (m :: Nat) + (n :: Nat) :: Nat

type family (m :: Nat) * (n :: Nat) :: Nat

type family (m :: Nat) ^ (n :: Nat) :: Nat

class (kparam ~ Kind) => SingE (kparam :: k) rep | kparam -> rep where fromSing :: Sing (a :: k) -> rep

instance SingE (Kind :: Nat) Integer where fromSing (SNat n) = n

instance SingE (Kind :: Symbol) String where fromSing (SSym s) = s

class (SingI a, SingE (Kind :: k) rep) => SingRep (a :: k) rep | a -> rep instance (SingI a, SingE (Kind :: k) rep) => SingRep (a :: k) rep

withSing :: SingI a => (Sing a -> b) -> b withSing f = f sing

singThat :: (SingRep a rep) => (rep -> Bool) -> Maybe (Sing a) singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing

instance (SingE (Kind :: k) rep, Show rep) => Show (Sing (a :: k)) where showsPrec p = showsPrec p . fromSing

instance (SingRep a rep, Read rep, Eq rep) => Read (Sing a) where readsPrec p cs = do (x,ys) <- readsPrec p cs case singThat (== x) of Just y -> [(y,ys)] Nothing -> []

data IsZero :: Nat -> * where IsZero :: IsZero 0 IsSucc :: !(Sing n) -> IsZero (n + 1)

isZero :: Sing n -> IsZero n isZero (SNat n) | n == 0 = unsafeCoerce IsZero | otherwise = unsafeCoerce (IsSucc (SNat (n1)))

instance Show (IsZero n) where show IsZero = "0" show (IsSucc n) = "(" ++ show n ++ " + 1)"

data IsEven :: Nat -> * where IsEvenZero :: IsEven 0 IsEven :: !(Sing (n+1)) -> IsEven (2 * n + 2) IsOdd :: !(Sing n) -> IsEven (2 * n + 1)

isEven :: Sing n -> IsEven n isEven (SNat n) | n == 0 = unsafeCoerce IsEvenZero | testBit n 0 = unsafeCoerce (IsOdd (SNat (n shiftR 1))) | otherwise = unsafeCoerce (IsEven (SNat (n shiftR 1)))

instance Show (IsEven n) where show IsEvenZero = "0" show (IsEven x) = "(2 * " ++ show x ++ ")" show (IsOdd x) = "(2 * " ++ show x ++ " + 1)"