Safe Haskell	None
Language	GHC2021

Data.Type.Nat.Singleton.Safe

Contents

Natural Number Singletons
Existential Wrapper
Laws
Linking Type-Level and Value-Level
Specialised target for conversion

Synopsis

data SNat (n :: Nat) where
- Z :: SNat 'Z
- S :: forall (n1 :: Nat). SNat n1 -> SNat ('S n1)
toSafe :: forall (n :: Nat). SNat n -> SNat n
fromSafe :: forall (n :: Nat). SNat 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 (m :: Nat) (n :: Nat). SNat m -> SNat n -> Maybe (m :~: n)
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

Natural Number Singletons

data SNat (n :: Nat) where Source #

SNat n is the singleton type for natural numbers.

Constructors

Z :: SNat 'Z
S :: forall (n1 :: Nat). SNat n1 -> SNat ('S n1)

Instances

Instances details

Show (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Safe 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.Safe Methods rnf :: SNat n -> () #
Eq (SNat n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Safe Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #

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

Convert from the efficient representation SNat to the safe representation SNat.

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

Convert from the safe representation SNat to the efficient representation SNat.

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 #

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

Addition for natural number singletons.

decSNat :: forall (m :: Nat) (n :: Nat). SNat m -> SNat n -> Maybe (m :~: n) 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.Safe Methods showsPrec :: Int -> SomeSNat -> ShowS # show :: SomeSNat -> String # showList :: [SomeSNat] -> ShowS #
NFData SomeSNat Source #
Instance details Defined in Data.Type.Nat.Singleton.Safe Methods rnf :: SomeSNat -> () #
Eq SomeSNat Source #
Instance details Defined in Data.Type.Nat.Singleton.Safe 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 SNatRep 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.Safe Methods natSing :: SNat 'Z Source #
KnownNat n => KnownNat ('S n) Source #
Instance details Defined in Data.Type.Nat.Singleton.Safe Methods natSing :: SNat ('S n) Source #

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

Specialised target for conversion

type SNatRep = Int #