Copyright | (C) 2014 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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
- class SNum a where
- (%+) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: a)
- (%-) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a)
- (%*) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t :: a)
- sNegate :: forall (t :: a). Sing t -> Sing (Apply NegateSym0 t :: a)
- sAbs :: forall (t :: a). Sing t -> Sing (Apply AbsSym0 t :: a)
- sSignum :: forall (t :: a). Sing t -> Sing (Apply SignumSym0 t :: a)
- sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t :: a)
- 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 #
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
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 # | |
SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((+@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506822 :: a6989586621679506802) Source # | |
data (+@#@$$) (arg6989586621679506822 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 6 Source #
Instances
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((+@#@$$) arg6989586621679506822 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((+@#@$$) arg6989586621679506822 :: TyFun a a -> Type) (arg6989586621679506823 :: a) Source # | |
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 # | |
SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((-@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506826 :: a6989586621679506802) Source # | |
data (-@#@$$) (arg6989586621679506826 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 6 Source #
Instances
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((-@#@$$) arg6989586621679506826 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((-@#@$$) arg6989586621679506826 :: TyFun a a -> Type) (arg6989586621679506827 :: a) Source # | |
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 # | |
SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((*@#@$) :: TyFun a6989586621679506802 (a6989586621679506802 ~> a6989586621679506802) -> Type) (arg6989586621679506830 :: a6989586621679506802) Source # | |
data (*@#@$$) (arg6989586621679506830 :: a6989586621679506802) :: (~>) a6989586621679506802 a6989586621679506802 infixl 7 Source #
Instances
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((*@#@$$) arg6989586621679506830 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply ((*@#@$$) arg6989586621679506830 :: TyFun a a -> Type) (arg6989586621679506831 :: a) Source # | |
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 # | |
Defined in Data.Singletons.Prelude.Num Methods sing :: Sing NegateSym0 Source # | |
SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679506834 :: a) Source # | |
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 # | |
SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679506836 :: a) Source # | |
data SignumSym0 :: forall a6989586621679506802. (~>) a6989586621679506802 a6989586621679506802 Source #
Instances
SNum a => SingI (SignumSym0 :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SignumSym0 Source # | |
SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679506802 a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679506838 :: a) Source # | |
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 # | |
Defined in Data.Singletons.Prelude.Num Methods | |
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679506802 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506840 :: Nat) Source # | |
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 # | |
Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SubtractSym0 Source # | |
SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679512259 (a6989586621679512259 ~> a6989586621679512259) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (SubtractSym0 :: TyFun a6989586621679512259 (a6989586621679512259 ~> a6989586621679512259) -> Type) (a6989586621679512263 :: a6989586621679512259) Source # | |
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 # | |
Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (SubtractSym1 d) Source # | |
SuppressUnusedWarnings (SubtractSym1 a6989586621679512263 :: TyFun a6989586621679512259 a6989586621679512259 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source # | |
type Apply (SubtractSym1 a6989586621679512263 :: TyFun a a -> Type) (a6989586621679512264 :: a) Source # | |
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 #