Copyright | (C) 2014 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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 a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009)
- data (+@#@$$) (arg6989586621679506029 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009
- type (+@#@$$$) (arg6989586621679506029 :: a6989586621679506009) (arg6989586621679506030 :: a6989586621679506009) = (+) arg6989586621679506029 arg6989586621679506030
- data (-@#@$) :: forall a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009)
- data (-@#@$$) (arg6989586621679506033 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009
- type (-@#@$$$) (arg6989586621679506033 :: a6989586621679506009) (arg6989586621679506034 :: a6989586621679506009) = (-) arg6989586621679506033 arg6989586621679506034
- data (*@#@$) :: forall a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009)
- data (*@#@$$) (arg6989586621679506037 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009
- type (*@#@$$$) (arg6989586621679506037 :: a6989586621679506009) (arg6989586621679506038 :: a6989586621679506009) = * arg6989586621679506037 arg6989586621679506038
- data NegateSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009
- type NegateSym1 (arg6989586621679506041 :: a6989586621679506009) = Negate arg6989586621679506041
- data AbsSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009
- type AbsSym1 (arg6989586621679506043 :: a6989586621679506009) = Abs arg6989586621679506043
- data SignumSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009
- type SignumSym1 (arg6989586621679506045 :: a6989586621679506009) = Signum arg6989586621679506045
- data FromIntegerSym0 :: forall a6989586621679506009. (~>) Nat a6989586621679506009
- type FromIntegerSym1 (arg6989586621679506047 :: Nat) = FromInteger arg6989586621679506047
- data SubtractSym0 :: forall a6989586621679511466. (~>) a6989586621679511466 ((~>) a6989586621679511466 a6989586621679511466)
- data SubtractSym1 (a6989586621679511470 :: a6989586621679511466) :: (~>) a6989586621679511466 a6989586621679511466
- type SubtractSym2 (a6989586621679511470 :: a6989586621679511466) (a6989586621679511471 :: a6989586621679511466) = Subtract a6989586621679511470 a6989586621679511471
Documentation
class PNum (a :: Type) Source #
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 #
(%+), (%*), sAbs, sSignum, sFromInteger
(%+) :: 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_6989586621679506057Sym0 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_6989586621679506065Sym0 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 a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009) infixl 6 Source #
Instances
SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) Source # | |
SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((+@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) (arg6989586621679506029 :: a6989586621679506009) Source # | |
data (+@#@$$) (arg6989586621679506029 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009 infixl 6 Source #
Instances
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((+@#@$$) arg6989586621679506029 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((+@#@$$) arg6989586621679506029 :: TyFun a a -> Type) (arg6989586621679506030 :: a) Source # | |
type (+@#@$$$) (arg6989586621679506029 :: a6989586621679506009) (arg6989586621679506030 :: a6989586621679506009) = (+) arg6989586621679506029 arg6989586621679506030 Source #
data (-@#@$) :: forall a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009) infixl 6 Source #
Instances
SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) Source # | |
SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((-@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) (arg6989586621679506033 :: a6989586621679506009) Source # | |
data (-@#@$$) (arg6989586621679506033 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009 infixl 6 Source #
Instances
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((-@#@$$) arg6989586621679506033 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((-@#@$$) arg6989586621679506033 :: TyFun a a -> Type) (arg6989586621679506034 :: a) Source # | |
type (-@#@$$$) (arg6989586621679506033 :: a6989586621679506009) (arg6989586621679506034 :: a6989586621679506009) = (-) arg6989586621679506033 arg6989586621679506034 Source #
data (*@#@$) :: forall a6989586621679506009. (~>) a6989586621679506009 ((~>) a6989586621679506009 a6989586621679506009) infixl 7 Source #
Instances
SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) Source # | |
SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((*@#@$) :: TyFun a6989586621679506009 (a6989586621679506009 ~> a6989586621679506009) -> Type) (arg6989586621679506037 :: a6989586621679506009) Source # | |
data (*@#@$$) (arg6989586621679506037 :: a6989586621679506009) :: (~>) a6989586621679506009 a6989586621679506009 infixl 7 Source #
Instances
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings ((*@#@$$) arg6989586621679506037 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply ((*@#@$$) arg6989586621679506037 :: TyFun a a -> Type) (arg6989586621679506038 :: a) Source # | |
type (*@#@$$$) (arg6989586621679506037 :: a6989586621679506009) (arg6989586621679506038 :: a6989586621679506009) = * arg6989586621679506037 arg6989586621679506038 Source #
data NegateSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009 Source #
Instances
SNum a => SingI (NegateSym0 :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num sing :: Sing NegateSym0 Source # | |
SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679506041 :: a) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679506041 :: a) = Negate arg6989586621679506041 |
type NegateSym1 (arg6989586621679506041 :: a6989586621679506009) = Negate arg6989586621679506041 Source #
data AbsSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009 Source #
Instances
SNum a => SingI (AbsSym0 :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679506043 :: a) Source # | |
data SignumSym0 :: forall a6989586621679506009. (~>) a6989586621679506009 a6989586621679506009 Source #
Instances
SNum a => SingI (SignumSym0 :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num sing :: Sing SignumSym0 Source # | |
SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679506009 a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679506045 :: a) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679506045 :: a) = Signum arg6989586621679506045 |
type SignumSym1 (arg6989586621679506045 :: a6989586621679506009) = Signum arg6989586621679506045 Source #
data FromIntegerSym0 :: forall a6989586621679506009. (~>) Nat a6989586621679506009 Source #
Instances
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num | |
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679506009 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506047 :: Nat) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679506047 :: Nat) = (FromInteger arg6989586621679506047 :: k2) |
type FromIntegerSym1 (arg6989586621679506047 :: Nat) = FromInteger arg6989586621679506047 Source #
data SubtractSym0 :: forall a6989586621679511466. (~>) a6989586621679511466 ((~>) a6989586621679511466 a6989586621679511466) Source #
Instances
SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num sing :: Sing SubtractSym0 Source # | |
SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679511466 (a6989586621679511466 ~> a6989586621679511466) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (SubtractSym0 :: TyFun a6989586621679511466 (a6989586621679511466 ~> a6989586621679511466) -> Type) (a6989586621679511470 :: a6989586621679511466) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym0 :: TyFun a6989586621679511466 (a6989586621679511466 ~> a6989586621679511466) -> Type) (a6989586621679511470 :: a6989586621679511466) = SubtractSym1 a6989586621679511470 |
data SubtractSym1 (a6989586621679511470 :: a6989586621679511466) :: (~>) a6989586621679511466 a6989586621679511466 Source #
Instances
(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num sing :: Sing (SubtractSym1 d) Source # | |
SuppressUnusedWarnings (SubtractSym1 a6989586621679511470 :: TyFun a6989586621679511466 a6989586621679511466 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Num suppressUnusedWarnings :: () Source # | |
type Apply (SubtractSym1 a6989586621679511470 :: TyFun a a -> Type) (a6989586621679511471 :: a) Source # | |
Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym1 a6989586621679511470 :: TyFun a a -> Type) (a6989586621679511471 :: a) = Subtract a6989586621679511470 a6989586621679511471 |
type SubtractSym2 (a6989586621679511470 :: a6989586621679511466) (a6989586621679511471 :: a6989586621679511466) = Subtract a6989586621679511470 a6989586621679511471 Source #