Safe Haskell	None
Language	GHC2021

Data.Type.Nat.Singleton.Fast

Contents

Natural Number Singletons
Existential Wrapper
Laws
Linking Type-Level and Value-Level
Fast

Synopsis

data SNat (n :: Nat) where
- pattern Z :: () => n ~ 'Z => SNat n
- pattern S :: () => Pos n => SNat (Pred n) -> SNat n
fromSNat :: forall i (n :: Nat). Integral i => SNat n -> i
fromSNatRaw :: forall (n :: Nat). SNat n -> SNatRep
plus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
decSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m)
data SomeSNat = SomeSNat !(SNat n)
withSomeSNat :: (forall (n :: Nat). SNat n -> a) -> SomeSNat -> a
toSomeSNat :: Integral i => i -> SomeSNat
toSomeSNatRaw :: SNatRep -> SomeSNat
fromSomeSNat :: Integral i => SomeSNat -> i
fromSomeSNatRaw :: SomeSNat -> SNatRep
plusUnitL :: forall (n :: Nat). Proxy n -> ('Z + n) :~: n
plusUnitR :: forall (n :: Nat). SNat n -> (n + 'Z) :~: n
plusCommS :: forall (n :: Nat) (m :: Nat). SNat n -> Proxy m -> 'S (n + m) :~: (n + 'S m)
plusComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n + m) :~: (m + n)
plusAssoc :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> Proxy m -> Proxy l -> ((n + m) + l) :~: (n + (m + l))
class KnownNat (n :: Nat) where
- natSing :: SNat n
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
type SNatRep = Int
intToSNatRep :: Int -> SNatRep
snatRepToInt :: SNatRep -> Int
newtype SNat (n :: Nat) = UnsafeSNat {
- snatRep :: SNatRep
}

Natural Number Singletons

data SNat (n :: Nat) where Source #

SNat n is the singleton type for natural numbers.

Bundled Patterns

pattern Z :: () => n ~ 'Z => SNat n
pattern S :: () => Pos n => SNat (Pred n) -> SNat n

Instances

Instances details

Show (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
NFData (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods rnf :: SNat n -> () #
Eq (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #

fromSNat :: forall i (n :: Nat). Integral i => SNat n -> i Source #

fromSNat n returns the numeric representation of 'SNat n'.

fromSNatRaw :: forall (n :: Nat). SNat n -> SNatRep Source #

fromSNatRaw n returns the raw underlying representation of 'SNat n'.

plus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m) Source #

Addition for natural number singletons.

decSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m) Source #

Decidable equality for natural number singletons.

Existential Wrapper

data SomeSNat Source #

An existential wrapper around natural number singletons.

Constructors

SomeSNat !(SNat n)

Instances

Instances details

Show SomeSNat Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods showsPrec :: Int -> SomeSNat -> ShowS # show :: SomeSNat -> String # showList :: [SomeSNat] -> ShowS #
NFData SomeSNat Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods rnf :: SomeSNat -> () #
Eq SomeSNat Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods (==) :: SomeSNat -> SomeSNat -> Bool # (/=) :: SomeSNat -> SomeSNat -> Bool #

withSomeSNat :: (forall (n :: Nat). SNat n -> a) -> SomeSNat -> a Source #

Evaluate a term with access to the underlying SNat.

toSomeSNat :: Integral i => i -> SomeSNat Source #

toSomeSNat n constructs the singleton SNat n.

toSomeSNat (fromSomeSNat n) == n

toSomeSNatRaw :: SNatRep -> SomeSNat Source #

toSomeSNat n constructs the singleton SNat n.

toSomeSNatRaw (fromSomeSNatRaw n) == n

fromSomeSNat :: Integral i => SomeSNat -> i Source #

fromSomeSNat n returns the numeric representation of the wrapped singleton.

fromSomeSNatRaw :: SomeSNat -> SNatRep Source #

fromSomeSNat n returns the numeric representation of the wrapped singleton.

Laws

plusUnitL :: forall (n :: Nat). Proxy n -> ('Z + n) :~: n Source #

plusUnitR :: forall (n :: Nat). SNat n -> (n + 'Z) :~: n Source #

plusCommS :: forall (n :: Nat) (m :: Nat). SNat n -> Proxy m -> 'S (n + m) :~: (n + 'S m) Source #

plusComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n + m) :~: (m + n) Source #

plusAssoc :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> Proxy m -> Proxy l -> ((n + m) + l) :~: (n + (m + l)) Source #

Linking Type-Level and Value-Level

class KnownNat (n :: Nat) where Source #

Methods

natSing :: SNat n Source #

Instances

Instances details

KnownNat 'Z Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods natSing :: SNat 'Z Source #
KnownNat n => KnownNat ('S n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods natSing :: SNat ('S n) Source #

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r Source #

Fast

type SNatRep = Int Source #

intToSNatRep :: Int -> SNatRep Source #

Convert an Int to an SNatRep.

snatRepToInt :: SNatRep -> Int Source #

Convert an SNatRep to an Int.

newtype SNat (n :: Nat) Source #

SNat n is the singleton type for natural numbers.

Constructors

UnsafeSNat
Fields snatRep :: SNatRep

Instances

Instances details

Show (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
NFData (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods rnf :: SNat n -> () #
Eq (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #