Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

Documentation

data Nat Source

Constructors

Z
S Nat

Instances

Eq Nat
Ord Nat
Show Nat
SingI Nat Z
POrd Nat (KProxy Nat)
SEq Nat (KProxy Nat)
PEq Nat (KProxy Nat)
SDecide Nat (KProxy Nat)
SingI Nat n0 => SingI Nat (S n)
SingKind Nat (KProxy Nat)
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> ) (:$$)
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$)
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:*$)
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:+$)
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0
data Sing Nat where SZ :: (~) Nat z Z => Sing Nat z SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z
type Compare Nat Z Z = EQ
type (:==) Nat a0 b0
type Apply Nat Nat SSym0 l0 = SSym1 l0
type Compare Nat Z (S rhs0) = LT
type Apply Nat Nat ((:*$$) l1) l0
type Apply Nat Nat ((:+$$) l1) l0
type DemoteRep Nat (KProxy Nat) = Nat
type Compare Nat (S lhs0) Z = GT
type Compare Nat (S lhs0) (S rhs0) = ThenCmp EQ (Compare Nat lhs0 rhs0)
type Apply (TyFun Nat Nat -> ) Nat (:$) l0 = (:*$$) l0
type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0

natPlus :: Nat -> Nat -> Nat Source

This is the plain value-level version of addition on Nats. There's rarely a reason to use this; it's included for completeness.

natMul :: Nat -> Nat -> Nat Source

Similarly to natPlus, this one is included for completeness.

type SNat z = Sing z Source

data family Sing a

The singleton kind-indexed data family.

Instances

SDecide k (KProxy k) => TestEquality k (Sing k)
data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Nat where SZ :: (~) Nat z Z => Sing Nat z SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

type family a :* a :: Nat Source

Equations

Z :* b = ZSym0
(S a) :* b = Apply (Apply (:+$) b) (Apply (Apply (:*$) a) b)

data (:*$) l Source

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:*$)
type Apply (TyFun Nat Nat -> ) Nat (:$) l0 = (:*$$) l0

data l :*$$ l Source

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> ) (:$$)
type Apply Nat Nat ((:*$$) l1) l0

type family a :+ a :: Nat Source

Equations

Z :+ b = b
(S a) :+ b = Apply SSym0 (Apply (Apply (:+$) a) b)

data (:+$) l Source

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:+$)
type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0

data l :+$$ l Source

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$)
type Apply Nat Nat ((:+$$) l1) l0

data SSym0 l Source

Constructors

forall arg . (KindOf (Apply SSym0 arg) ~ KindOf (SSym1 arg)) => SSym0KindInference

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0
type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t Source

type ZSym0 = Z Source

(%:+) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t) Source

(%:*) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:*$) t) t) Source

type family Lit n 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))

type SLit n = Sing (Lit n) Source