Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

data Nat
- = Z
- | S Nat
type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ...
type family NatMul (a :: Nat) (a :: Nat) :: Nat where ...
type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ...
type family NatAbs (a :: Nat) :: Nat where ...
type family NatSignum (a :: Nat) :: Nat where ...
natPlus :: Nat -> Nat -> Nat
natMul :: Nat -> Nat -> Nat
natMinus :: Nat -> Nat -> Nat
natAbs :: Nat -> Nat
natSignum :: Nat -> Nat
someNatVal :: Integer -> Maybe (SomeSing Nat)
type SNat = (Sing :: Nat -> Type)
data family Sing (a :: k) :: *
class PNum a
class SNum a
data SSym0 (l :: TyFun Nat Nat) = SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0KindInference
type SSym1 (t :: Nat) = S t
type ZSym0 = Z
type family Lit n where ...
data LitSym0 (l :: TyFun Nat Nat) = SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0KindInference
type LitSym1 (t :: Nat) = Lit t
type SLit n = Sing (Lit n)
sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)

Documentation

data Nat Source #

Constructors

Z
S Nat

Instances

Eq Nat Source #
Instance details Defined in Data.Nat Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Num Nat Source #
Instance details Defined in Data.Nat Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Instance details Defined in Data.Nat Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Show Nat Source #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
PShow Nat Source #
Instance details Defined in Data.Nat Associated Types type ShowsPrec arg arg1 arg2 :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg1 :: Symbol #
SShow Nat => SShow Nat Source #
Instance details Defined in Data.Nat Methods sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #
PNum Nat Source #
Instance details Defined in Data.Nat Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
SNum Nat Source #
Instance details Defined in Data.Nat Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
ShowSing Nat => ShowSing Nat Source #
Instance details Defined in Data.Nat Methods showsSingPrec :: Int -> Sing a -> ShowS #
POrd Nat Source #
Instance details Defined in Data.Nat Associated Types type Compare arg arg1 :: Ordering # type arg < arg1 :: Bool # type arg <= arg1 :: Bool # type arg > arg1 :: Bool # type arg >= arg1 :: Bool # type Max arg arg1 :: a # type Min arg arg1 :: a #
SOrd Nat => SOrd Nat Source #
Instance details Defined in Data.Nat Methods sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) # (%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) # (%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) # (%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) # (%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) # sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) # sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #
SEq Nat => SEq Nat Source #
Instance details Defined in Data.Nat Methods (%==) :: Sing a -> Sing b -> Sing (a == b) # (%/=) :: Sing a -> Sing b -> Sing (a /= b) #
PEq Nat Source #
Instance details Defined in Data.Nat Associated Types type x == y :: Bool # type x /= y :: Bool #
SDecide Nat => SDecide Nat Source #
Instance details Defined in Data.Nat Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SingKind Nat Source #
Instance details Defined in Data.Nat Associated Types type Demote Nat = (r :: *) # Methods fromSing :: Sing a -> Demote Nat # toSing :: Demote Nat -> SomeSing Nat #
SingI Z Source #
Instance details Defined in Data.Nat Methods sing :: Sing Z #
SingI n => SingI (S n :: Nat) Source #
Instance details Defined in Data.Nat Methods sing :: Sing (S n) #
Eq (SNat n) Source #
Instance details Defined in Data.Nat Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) Source #
Instance details Defined in Data.Nat Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
ShowSing Nat => Show (Sing z) Source #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
SuppressUnusedWarnings LitSym0 Source #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
data Sing (z :: Nat) Source #
Instance details Defined in Data.Nat data Sing (z :: Nat) where SZ :: Sing Z SS :: Sing (S n)
type Demote Nat Source #
Instance details Defined in Data.Nat type Demote Nat = Nat
type Show_ (arg :: Nat) Source #
Instance details Defined in Data.Nat type Show_ (arg :: Nat) = Apply (Show__6989586621679675935Sym0 :: TyFun Nat Symbol -> *) arg
type FromInteger a Source #
Instance details Defined in Data.Nat type FromInteger a
type Signum (a :: Nat) Source #
Instance details Defined in Data.Nat type Signum (a :: Nat)
type Abs (a :: Nat) Source #
Instance details Defined in Data.Nat type Abs (a :: Nat)
type Negate (arg :: Nat) Source #
Instance details Defined in Data.Nat type Negate (arg :: Nat) = Apply (Negate_6989586621679412401Sym0 :: TyFun Nat Nat -> *) arg
type ShowList (arg :: [Nat]) arg1 Source #
Instance details Defined in Data.Nat type ShowList (arg :: [Nat]) arg1 = Apply (Apply (ShowList_6989586621679675953Sym0 :: TyFun [Nat] (TyFun Symbol Symbol -> Type) -> *) arg) arg1
type (a1 :: Nat) * (a2 :: Nat) Source #
Instance details Defined in Data.Nat type (a1 :: Nat) * (a2 :: Nat)
type (a1 :: Nat) - (a2 :: Nat) Source #
Instance details Defined in Data.Nat type (a1 :: Nat) - (a2 :: Nat)
type (a1 :: Nat) + (a2 :: Nat) Source #
Instance details Defined in Data.Nat type (a1 :: Nat) + (a2 :: Nat)
type Min (arg :: Nat) (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type Min (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg) arg1
type Max (arg :: Nat) (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type Max (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg) arg1
type (arg :: Nat) >= (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type (arg :: Nat) >= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679300637Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg) arg1
type (arg :: Nat) > (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type (arg :: Nat) > (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679300604Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg) arg1
type (arg :: Nat) <= (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type (arg :: Nat) <= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg) arg1
type (arg :: Nat) < (arg1 :: Nat) Source #
Instance details Defined in Data.Nat type (arg :: Nat) < (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679300538Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg) arg1
type Compare (a1 :: Nat) (a2 :: Nat) Source #
Instance details Defined in Data.Nat type Compare (a1 :: Nat) (a2 :: Nat)
type (x :: Nat) /= (y :: Nat) Source #
Instance details Defined in Data.Nat type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (a :: Nat) == (b :: Nat) Source #
Instance details Defined in Data.Nat type (a :: Nat) == (b :: Nat)
type ShowsPrec a1 (a2 :: Nat) a3 Source #
Instance details Defined in Data.Nat type ShowsPrec a1 (a2 :: Nat) a3
type Apply LitSym0 (l :: Nat) Source #
Instance details Defined in Data.Nat type Apply LitSym0 (l :: Nat) = Lit l
type Apply SSym0 (l :: Nat) Source #
Instance details Defined in Data.Nat type Apply SSym0 (l :: Nat) = S l

type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ... Source #

Equations

NatPlus Z b = b
NatPlus (S a) b = Apply SSym0 (Apply (Apply NatPlusSym0 a) b)

type family NatMul (a :: Nat) (a :: Nat) :: Nat where ... Source #

Equations

NatMul Z _ = ZSym0
NatMul (S a) b = Apply (Apply NatPlusSym0 b) (Apply (Apply NatMulSym0 a) b)

type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ... Source #

Equations

NatMinus Z _ = ZSym0
NatMinus (S a) (S b) = Apply (Apply NatMinusSym0 a) b
NatMinus a Z = a

type family NatAbs (a :: Nat) :: Nat where ... Source #

Equations

NatAbs n = n

type family NatSignum (a :: Nat) :: Nat where ... Source #

Equations

NatSignum Z = ZSym0
NatSignum (S _) = Apply SSym0 ZSym0

natPlus :: Nat -> Nat -> Nat Source #

natMul :: Nat -> Nat -> Nat Source #

natMinus :: Nat -> Nat -> Nat Source #

natAbs :: Nat -> Nat Source #

natSignum :: Nat -> Nat Source #

someNatVal :: Integer -> Maybe (SomeSing Nat) Source #

Converts a runtime Integer to an existentially wrapped Nat. Returns Nothing if the argument is negative

type SNat = (Sing :: Nat -> Type) Source #

data family Sing (a :: k) :: * #

The singleton kind-indexed data family.

Instances

Eq (SNat n) #
Instance details Defined in Data.Nat Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #
Instance details Defined in Data.Nat Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
ShowSing Nat => Show (Sing z) #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (z :: Bool)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Bool) where SFalse :: Sing False STrue :: Sing True
data Sing (z :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Ordering) where SLT :: Sing LT SEQ :: Sing EQ SGT :: Sing GT
data Sing (n :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: Sing n
data Sing (n :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: Sing n
data Sing (z :: ())
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: ()) where STuple0 :: Sing ()
data Sing (z :: Nat) #
Instance details Defined in Data.Nat data Sing (z :: Nat) where SZ :: Sing Z SS :: Sing (S n)
data Sing (z :: Void)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Void)
data Sing (z :: [a])
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: [a]) where SNil :: Sing ([] :: [a]) SCons :: Sing (n1 ': n2)
data Sing (z :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Maybe a) where SNothing :: Sing (Nothing :: Maybe a) SJust :: Sing (Just n)
data Sing (z :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: NonEmpty a) where (:%\|) :: Sing (n1 :\| n2)
data Sing (z :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Either a b) where SLeft :: Sing (Left n :: Either a b) SRight :: Sing (Right n :: Either a b)
data Sing (z :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b)) where STuple2 :: Sing ((,) n1 n2)
data Sing (f :: k1 ~> k2)
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (z :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c)) where STuple3 :: Sing ((,,) n1 n2 n3)
data Sing (z :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d)) where STuple4 :: Sing ((,,,) n1 n2 n3 n4)
data Sing (z :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e)) where STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (z :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f)) where STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (z :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f, g)) where STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

class PNum a #

Instances

PNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
PNum Nat #
Instance details Defined in Data.Nat Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #

class SNum a #

Minimal complete definition

(%+), (%*), sAbs, sSignum, sFromInteger

Instances

SNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
SNum Nat #
Instance details Defined in Data.Nat Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

data SSym0 (l :: TyFun Nat Nat) Source #

Constructors

SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0KindInference

Instances

SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
type Apply SSym0 (l :: Nat) Source #
Instance details Defined in Data.Nat type Apply SSym0 (l :: Nat) = S l

type SSym1 (t :: Nat) = S t Source #

type ZSym0 = Z Source #

type family Lit n where ... Source #

Provides a shorthand for Nat-s using GHC.TypeLits, for example:

>>> :kind! Lit 3
Lit 3 :: Nat
= 'S ('S ('S 'Z))

Equations

Lit 0 = Z
Lit n = S (Lit (n - 1))

data LitSym0 (l :: TyFun Nat Nat) Source #

Constructors

SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0KindInference

Instances

SuppressUnusedWarnings LitSym0 Source #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
type Apply LitSym0 (l :: Nat) Source #
Instance details Defined in Data.Nat type Apply LitSym0 (l :: Nat) = Lit l

type LitSym1 (t :: Nat) = Lit t Source #

type SLit n = Sing (Lit n) Source #

sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n) Source #

Shorthand for SNat literals using TypeApplications.

>>> :set -XTypeApplications
>>> sLit @5
SS (SS (SS (SS (SS SZ))))