singletons-2.5.1: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Num

Contents

Description

Defines and exports promoted and singleton versions of definitions from GHC.Num.

Be warned that some of the associated type families in the PNum class ((+), (-), and (*)) clash with their counterparts for Nat in the GHC.TypeLits module.

Synopsis
  • class PNum (a :: Type) where
    • type (arg :: a) + (arg :: a) :: a
    • type (arg :: a) - (arg :: a) :: a
    • type (arg :: a) * (arg :: a) :: a
    • type Negate (arg :: a) :: a
    • type Abs (arg :: a) :: a
    • type Signum (arg :: a) :: a
    • type FromInteger (arg :: Nat) :: a
  • class SNum a where
  • type family Subtract (a :: a) (a :: a) :: a where ...
  • sSubtract :: forall a (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)
  • data (+@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802)
  • data (+@#@$$) (arg6989586621679506822 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802
  • type (+@#@$$$) (arg6989586621679506822 :: a6989586621679506802) (arg6989586621679506823 :: a6989586621679506802) = (+) arg6989586621679506822 arg6989586621679506823
  • data (-@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802)
  • data (-@#@$$) (arg6989586621679506826 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802
  • type (-@#@$$$) (arg6989586621679506826 :: a6989586621679506802) (arg6989586621679506827 :: a6989586621679506802) = (-) arg6989586621679506826 arg6989586621679506827
  • data (*@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802)
  • data (*@#@$$) (arg6989586621679506830 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802
  • type (*@#@$$$) (arg6989586621679506830 :: a6989586621679506802) (arg6989586621679506831 :: a6989586621679506802) = * arg6989586621679506830 arg6989586621679506831
  • data NegateSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802
  • type NegateSym1 (arg6989586621679506834 :: a6989586621679506802) = Negate arg6989586621679506834
  • data AbsSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802
  • type AbsSym1 (arg6989586621679506836 :: a6989586621679506802) = Abs arg6989586621679506836
  • data SignumSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802
  • type SignumSym1 (arg6989586621679506838 :: a6989586621679506802) = Signum arg6989586621679506838
  • data FromIntegerSym0 :: forall a6989586621679506802. (~>) Nat a6989586621679506802
  • type FromIntegerSym1 (arg6989586621679506840 :: Nat) = FromInteger arg6989586621679506840
  • data SubtractSym0 :: forall a6989586621679512259. (~>) a6989586621679512259 ((~>) a6989586621679512259 a6989586621679512259)
  • data SubtractSym1 (a6989586621679512263 :: a6989586621679512259) :: (~>) a6989586621679512259 a6989586621679512259
  • type SubtractSym2 (a6989586621679512263 :: a6989586621679512259) (a6989586621679512264 :: a6989586621679512259) = Subtract a6989586621679512263 a6989586621679512264

Documentation

class PNum (a :: Type) Source #

Associated Types

type (arg :: a) + (arg :: a) :: a infixl 6 Source #

type (arg :: a) - (arg :: a) :: a infixl 6 Source #

type (arg :: a) * (arg :: a) :: a infixl 7 Source #

type Negate (arg :: a) :: a Source #

type Abs (arg :: a) :: a Source #

type Signum (arg :: a) :: a Source #

type FromInteger (arg :: Nat) :: a Source #

Instances
PNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Identity

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

PNum (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type arg + arg :: a Source #

type arg - arg :: a Source #

type arg * arg :: a Source #

type Negate arg :: a Source #

type Abs arg :: a Source #

type Signum arg :: a Source #

type FromInteger arg :: a Source #

class SNum a where Source #

Minimal complete definition

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

Methods

(%+) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: a) infixl 6 Source #

(%-) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a) infixl 6 Source #

(%*) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t :: a) infixl 7 Source #

sNegate :: forall (t :: a). Sing t -> Sing (Apply NegateSym0 t :: a) Source #

sAbs :: forall (t :: a). Sing t -> Sing (Apply AbsSym0 t :: a) Source #

sSignum :: forall (t :: a). Sing t -> Sing (Apply SignumSym0 t :: a) Source #

sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t :: a) Source #

(%-) :: forall (t :: a) (t :: a). (Apply (Apply (-@#@$) t) t :: a) ~ Apply (Apply TFHelper_6989586621679506850Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a) infixl 6 Source #

sNegate :: forall (t :: a). (Apply NegateSym0 t :: a) ~ Apply Negate_6989586621679506858Sym0 t => Sing t -> Sing (Apply NegateSym0 t :: a) Source #

Instances
SNum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SNum a => SNum (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SNum a => SNum (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SNum a => SNum (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Identity

SNum a => SNum (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SNum a => SNum (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SNum a => SNum (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SNum a => SNum (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

type family Subtract (a :: a) (a :: a) :: a where ... Source #

Equations

Subtract x y = Apply (Apply (-@#@$) y) x 

sSubtract :: forall a (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a) Source #

Defunctionalization symbols

data (+@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802) infixl 6 Source #

Instances
SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506822 :: a6989586621679506802) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506822 :: a6989586621679506802) = (+@#@$$) arg6989586621679506822

data (+@#@$$) (arg6989586621679506822 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 6 Source #

Instances
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((+@#@$$) d) Source #

SuppressUnusedWarnings ((+@#@$$) arg6989586621679506822 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$$) arg6989586621679506822 :: TyFun a a -> Type) (arg6989586621679506823 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$$) arg6989586621679506822 :: TyFun a a -> Type) (arg6989586621679506823 :: a) = arg6989586621679506822 + arg6989586621679506823

type (+@#@$$$) (arg6989586621679506822 :: a6989586621679506802) (arg6989586621679506823 :: a6989586621679506802) = (+) arg6989586621679506822 arg6989586621679506823 Source #

data (-@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802) infixl 6 Source #

Instances
SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506826 :: a6989586621679506802) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506826 :: a6989586621679506802) = (-@#@$$) arg6989586621679506826

data (-@#@$$) (arg6989586621679506826 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 6 Source #

Instances
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((-@#@$$) d) Source #

SuppressUnusedWarnings ((-@#@$$) arg6989586621679506826 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$$) arg6989586621679506826 :: TyFun a a -> Type) (arg6989586621679506827 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$$) arg6989586621679506826 :: TyFun a a -> Type) (arg6989586621679506827 :: a) = arg6989586621679506826 - arg6989586621679506827

type (-@#@$$$) (arg6989586621679506826 :: a6989586621679506802) (arg6989586621679506827 :: a6989586621679506802) = (-) arg6989586621679506826 arg6989586621679506827 Source #

data (*@#@$) :: forall a6989586621679506802. (~>) a6989586621679506802 ((~>) a6989586621679506802 a6989586621679506802) infixl 7 Source #

Instances
SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506830 :: a6989586621679506802) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506830 :: a6989586621679506802) = (*@#@$$) arg6989586621679506830

data (*@#@$$) (arg6989586621679506830 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 7 Source #

Instances
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((*@#@$$) d) Source #

SuppressUnusedWarnings ((*@#@$$) arg6989586621679506830 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$$) arg6989586621679506830 :: TyFun a a -> Type) (arg6989586621679506831 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$$) arg6989586621679506830 :: TyFun a a -> Type) (arg6989586621679506831 :: a) = arg6989586621679506830 * arg6989586621679506831

type (*@#@$$$) (arg6989586621679506830 :: a6989586621679506802) (arg6989586621679506831 :: a6989586621679506802) = * arg6989586621679506830 arg6989586621679506831 Source #

data NegateSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802 Source #

Instances
SNum a => SingI (NegateSym0 :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679506834 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679506834 :: a) = Negate arg6989586621679506834

type NegateSym1 (arg6989586621679506834 :: a6989586621679506802) = Negate arg6989586621679506834 Source #

data AbsSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802 Source #

Instances
SNum a => SingI (AbsSym0 :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679506836 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679506836 :: a) = Abs arg6989586621679506836

type AbsSym1 (arg6989586621679506836 :: a6989586621679506802) = Abs arg6989586621679506836 Source #

data SignumSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802 Source #

Instances
SNum a => SingI (SignumSym0 :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679506838 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679506838 :: a) = Signum arg6989586621679506838

type SignumSym1 (arg6989586621679506838 :: a6989586621679506802) = Signum arg6989586621679506838 Source #

data FromIntegerSym0 :: forall a6989586621679506802. (~>) Nat a6989586621679506802 Source #

Instances
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679506802 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506840 :: Nat) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506840 :: Nat) = (FromInteger arg6989586621679506840 :: k2)

type FromIntegerSym1 (arg6989586621679506840 :: Nat) = FromInteger arg6989586621679506840 Source #

data SubtractSym0 :: forall a6989586621679512259. (~>) a6989586621679512259 ((~>) a6989586621679512259 a6989586621679512259) Source #

Instances
SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679512259 (a6989586621679512259 ~> a6989586621679512259) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SubtractSym0 :: TyFun a6989586621679512259 (a6989586621679512259 ~> a6989586621679512259) -> Type) (a6989586621679512263 :: a6989586621679512259) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SubtractSym0 :: TyFun a6989586621679512259 (a6989586621679512259 ~> a6989586621679512259) -> Type) (a6989586621679512263 :: a6989586621679512259) = SubtractSym1 a6989586621679512263

data SubtractSym1 (a6989586621679512263 :: a6989586621679512259) :: (~>) a6989586621679512259 a6989586621679512259 Source #

Instances
(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d) Source #

SuppressUnusedWarnings (SubtractSym1 a6989586621679512263 :: TyFun a6989586621679512259 a6989586621679512259 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SubtractSym1 a6989586621679512263 :: TyFun a a -> Type) (a6989586621679512264 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

type Apply (SubtractSym1 a6989586621679512263 :: TyFun a a -> Type) (a6989586621679512264 :: a) = Subtract a6989586621679512263 a6989586621679512264

type SubtractSym2 (a6989586621679512263 :: a6989586621679512259) (a6989586621679512264 :: a6989586621679512259) = Subtract a6989586621679512263 a6989586621679512264 Source #