Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Num

Contents

Defunctionalization symbols

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 (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)
data (+@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) +@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (+@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (+) t t
data (-@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) -@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (-@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (-) t t
data (*@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) *@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (*@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = * t t
data NegateSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type NegateSym1 (t :: a6989586621679428868) = Negate t
data AbsSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type AbsSym1 (t :: a6989586621679428868) = Abs t
data SignumSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type SignumSym1 (t :: a6989586621679428868) = Signum t
data FromIntegerSym0 (l :: TyFun Nat a6989586621679428868)
type FromIntegerSym1 (t :: Nat) = FromInteger t
data SubtractSym0 (l :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type))
data SubtractSym1 (l :: a6989586621679431141) (l :: TyFun a6989586621679431141 a6989586621679431141)
type SubtractSym2 (t :: a6989586621679431141) (t :: a6989586621679431141) = Subtract t t

Documentation

class PNum (a :: Type) #

Associated Types

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 #

Instances

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

class SNum a where #

Minimal complete definition

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

Methods

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

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

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

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) #

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

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

Instances

SNum Nat #

Instance details

Defined in Data.Singletons.Prelude.Num

Methods

(%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) #

(%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) #

(%*) :: Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) #

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) #

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

Equations

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

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

Defunctionalization symbols

data (+@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type)) #

Instances

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((+@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) (l :: a6989586621679428868) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) (l :: a6989586621679428868) = (+@#@$$) l

data (l :: a6989586621679428868) +@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings ((+@#@$$) :: a6989586621679428868 -> TyFun a6989586621679428868 a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

type (+@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (+) t t #

data (-@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type)) #

Instances

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((-@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) (l :: a6989586621679428868) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> *) (l :: a6989586621679428868) = (-@#@$$) l

data (l :: a6989586621679428868) -@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings ((-@#@$$) :: a6989586621679428868 -> TyFun a6989586621679428868 a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

type (-@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (-) t t #

data (*@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type)) #

Instances

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) (l :: a6989586621679428868) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) (l :: a6989586621679428868) = (*@#@$$) l

data (l :: a6989586621679428868) *@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings ((@#@$$) :: a6989586621679428868 -> TyFun a6989586621679428868 a6989586621679428868 -> ) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2

type (*@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = * t t #

data NegateSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679428868 a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (NegateSym0 :: TyFun a a -> *) (l :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (NegateSym0 :: TyFun a a -> *) (l :: a) = Negate l

type NegateSym1 (t :: a6989586621679428868) = Negate t #

data AbsSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679428868 a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (AbsSym0 :: TyFun a a -> *) (l :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (AbsSym0 :: TyFun a a -> *) (l :: a) = Abs l

type AbsSym1 (t :: a6989586621679428868) = Abs t #

data SignumSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679428868 a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (SignumSym0 :: TyFun a a -> *) (l :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SignumSym0 :: TyFun a a -> *) (l :: a) = Signum l

type SignumSym1 (t :: a6989586621679428868) = Signum t #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679428868) #

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)

type FromIntegerSym1 (t :: Nat) = FromInteger t #

data SubtractSym0 (l :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type)) #

Instances

SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (SubtractSym0 :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type) -> *) (l :: a6989586621679431141) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym0 :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type) -> *) (l :: a6989586621679431141) = SubtractSym1 l

data SubtractSym1 (l :: a6989586621679431141) (l :: TyFun a6989586621679431141 a6989586621679431141) #

Instances

SuppressUnusedWarnings (SubtractSym1 :: a6989586621679431141 -> TyFun a6989586621679431141 a6989586621679431141 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a) = Subtract l1 l2

type SubtractSym2 (t :: a6989586621679431141) (t :: a6989586621679431141) = Subtract t t #

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) (l :: a6989586621679428868) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type) -> ) (l :: a6989586621679428868) = (*@#@$$) l

SuppressUnusedWarnings ((@#@$$) :: a6989586621679428868 -> TyFun a6989586621679428868 a6989586621679428868 -> ) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2