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

Documentation

class PNum (a :: Type) Source #

Associated Types

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

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

type (arg :: a) * (arg :: a) :: a 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 #

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_6989586621679440320Sym0 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_6989586621679440335Sym0 t) => Sing t -> Sing (Apply NegateSym0 t :: a) Source #

Instances

SNum Nat Source #

Instance details

Defined in Data.Singletons.Prelude.Num

Methods

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

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

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

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

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

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

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) Source #

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

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

Defunctionalization symbols

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

Instances

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

data (l :: a6989586621679440260) +@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type (+@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (+) t t Source #

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

Instances

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

data (l :: a6989586621679440260) -@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type (-@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (-) t t Source #

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

Instances

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

data (l :: a6989586621679440260) *@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type (*@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = * t t Source #

data NegateSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type NegateSym1 (t :: a6989586621679440260) = Negate t Source #

data AbsSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type AbsSym1 (t :: a6989586621679440260) = Abs t Source #

data SignumSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

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

type SignumSym1 (t :: a6989586621679440260) = Signum t Source #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679440260) Source #

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) Source #
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 Source #

data SubtractSym0 (l :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type)) Source #

Instances

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

data SubtractSym1 (l :: a6989586621679442533) (l :: TyFun a6989586621679442533 a6989586621679442533) Source #

Instances

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

type SubtractSym2 (t :: a6989586621679442533) (t :: a6989586621679442533) = Subtract t t Source #

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

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