Type.Data.Num.Decimal.Number

Documentation

data Decimal

Representation name for decimal type level numbers.

Instances

Representation Decimal

type One Decimal

decimal :: Proxy n -> Proxy (Dec n)

data Dec x

The wrapper type for decimal type level numbers.

Instances

Integer x => Integer (Dec x)

(:/=:) x y => (Dec x) :/=: (Dec y)

(:==:) x y => (Dec x) :==: (Dec y)

(:>:) x y => (Dec x) :>: (Dec y)

(:>=:) x y => (Dec x) :>=: (Dec y)

(:<=:) x y => (Dec x) :<=: (Dec y)

(:<:) x y => (Dec x) :<: (Dec y)

type Repr (Dec x) = Decimal

type Log2Ceil (Dec x) = Dec (Log2Ceil x)

type Pow2 (Dec x) = Dec (Pow2 x)

type Div2 (Dec x)

type Mul2 (Dec x) = Dec ((:+:) x x)

type IsEven (Dec x) = IsEven x

type Pred (Dec x) = Dec (Pred x)

type Succ (Dec x) = Dec (Succ x)

type IsNatural (Dec x)

type IsNegative (Dec x)

type IsZero (Dec x)

type IsPositive (Dec x)

type Negate (Dec x)

type Compare (Dec x) (Dec y) = Compare x y

type (Dec x) :*: (Dec y) = Dec ((:*:) x y)

type (Dec x) :-: (Dec y) = Dec ((:-:) x y)

type (Dec x) :+: (Dec y) = Dec ((:+:) x y)

data Zero

Instances

Natural Zero

Integer Zero

Zero :==: Zero

Zero :>=: Zero

Zero :<=: Zero

Zero :/=: (Pos y ys)

Zero :/=: (Neg y ys)

Zero :>: (Neg y ys)

Zero :>=: (Neg y ys)

Zero :<=: (Pos y ys)

Zero :<: (Pos y ys)

(Pos x xs) :/=: Zero

(Neg x xs) :/=: Zero

(Pos x xs) :>: Zero

(Pos x xs) :>=: Zero

(Neg x xs) :<=: Zero

(Neg x xs) :<: Zero

type ToUnary Zero = Zero

type Pow2 Zero

type IsEven Zero = True

type Pred Zero = Neg Dec1 EndDesc

type Succ Zero

type Compare Zero Zero = EQ

type Zero :*: x = Zero

type Zero :+: y = y

type Compare Zero (Pos y ys) = LT

type Compare Zero (Neg y ys) = GT

type Compare (Pos x xs) Zero = GT

type Compare (Neg x xs) Zero = LT

type (Pos x xs) :*: Zero = Zero

type (Neg x xs) :*: Zero = Zero

type (Pos x xs) :+: Zero = Pos x xs

type (Neg x xs) :+: Zero = Neg x xs

data Pos x xs

Instances

Zero :/=: (Pos y ys)

Zero :<=: (Pos y ys)

Zero :<: (Pos y ys)

(Pos x, Digits xs) => Positive (Pos x xs)

(Pos x, Digits xs) => Natural (Pos x xs)

(Pos x, Digits xs) => Integer (Pos x xs)

(Pos x xs) :/=: Zero

(Pos x xs) :>: Zero

(Pos x xs) :>=: Zero

(~) * (IsEQ (ComparePos x xs y ys)) False => (Pos x xs) :/=: (Pos y ys)

(Pos x xs) :/=: (Neg y ys)

(Neg x xs) :/=: (Pos y ys)

(~) * (ComparePos x xs y ys) EQ => (Pos x xs) :==: (Pos y ys)

(~) * (ComparePos x xs y ys) GT => (Pos x xs) :>: (Pos y ys)

(Pos x xs) :>: (Neg y ys)

(~) * (GreaterPos y ys x xs) False => (Pos x xs) :>=: (Pos y ys)

(Pos x xs) :>=: (Neg y ys)

(~) * (GreaterPos x xs y ys) False => (Pos x xs) :<=: (Pos y ys)

(Neg x xs) :<=: (Pos y ys)

(~) * (ComparePos x xs y ys) LT => (Pos x xs) :<: (Pos y ys)

(Neg x xs) :<: (Pos y ys)

type Compare Zero (Pos y ys) = LT

type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs

type Log2Ceil (Pos x xs)

type Pow2 (Pos x xs)

type IsEven (Pos x xs)

type Pred (Pos x xs)

type Succ (Pos x xs)

type Compare (Pos x xs) Zero = GT

type (Pos x xs) :*: Zero = Zero

type (Pos x xs) :+: Zero = Pos x xs

type Compare (Pos x xs) (Neg y ys) = GT

type Compare (Pos x xs) (Pos y ys)

type Compare (Neg x xs) (Pos y ys) = LT

type (Pos x xs) :*: (Neg y ys)

type (Pos x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Pos y ys)

type (Pos x xs) :+: (Neg y ys)

type (Pos x xs) :+: (Pos y ys)

type (Neg x xs) :+: (Pos y ys)

data Neg x xs

Instances

Zero :/=: (Neg y ys)

Zero :>: (Neg y ys)

Zero :>=: (Neg y ys)

(Pos x, Digits xs) => Negative (Neg x xs)

(Pos x, Digits xs) => Integer (Neg x xs)

(Neg x xs) :/=: Zero

(Neg x xs) :<=: Zero

(Neg x xs) :<: Zero

(Pos x xs) :/=: (Neg y ys)

(~) * (IsEQ (ComparePos x xs y ys)) False => (Neg x xs) :/=: (Neg y ys)

(Neg x xs) :/=: (Pos y ys)

(~) * (ComparePos x xs y ys) EQ => (Neg x xs) :==: (Neg y ys)

(Pos x xs) :>: (Neg y ys)

(~) * (ComparePos x xs y ys) LT => (Neg x xs) :>: (Neg y ys)

(Pos x xs) :>=: (Neg y ys)

(~) * (GreaterPos x xs y ys) False => (Neg x xs) :>=: (Neg y ys)

(~) * (GreaterPos y ys x xs) False => (Neg x xs) :<=: (Neg y ys)

(Neg x xs) :<=: (Pos y ys)

(~) * (ComparePos x xs y ys) GT => (Neg x xs) :<: (Neg y ys)

(Neg x xs) :<: (Pos y ys)

type Compare Zero (Neg y ys) = GT

type IsEven (Neg x xs)

type Pred (Neg x xs)

type Succ (Neg x xs)

type Compare (Neg x xs) Zero = LT

type (Neg x xs) :*: Zero = Zero

type (Neg x xs) :+: Zero = Neg x xs

type Compare (Pos x xs) (Neg y ys) = GT

type Compare (Neg x xs) (Pos y ys) = LT

type Compare (Neg x xs) (Neg y ys)

type (Pos x xs) :*: (Neg y ys)

type (Neg x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Neg y ys)

type (Pos x xs) :+: (Neg y ys)

type (Neg x xs) :+: (Pos y ys)

type (Neg x xs) :+: (Neg y ys)

data EndAsc

The terminator type for ascending decimal digit lists.

Instances

Show EndAsc

data ds :< d infixl 9

data EndDesc

The terminator type for descending decimal digit lists.

Instances

Show EndDesc

Digits EndDesc

type ToUnaryAcc m EndDesc = m

data d :> ds infixr 9

Instances

(C xh, Digits xl) => Digits ((:>) xh xl)

type ToUnaryAcc m ((:>) x xs) = ToUnaryAcc (UnaryAcc m x) xs

newtype Singleton x

Constructors

Singleton Integer

singleton :: Integer x => Singleton x

singletonFromProxy :: Integer n => Proxy n -> Singleton n

integerFromSingleton :: Integer n => Singleton n -> Integer

integralFromSingleton :: (Integer n, Num a) => Singleton n -> a

integralFromProxy :: (Integer n, Num a) => Proxy n -> a

class Integer n where

Methods

switch :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n

Instances

Integer Zero

(Pos x, Digits xs) => Integer (Pos x xs)

(Pos x, Digits xs) => Integer (Neg x xs)

class Integer n => Natural n where

Methods

switchNat :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n

Instances

Natural Zero

(Pos x, Digits xs) => Natural (Pos x xs)

class Natural n => Positive n where

Methods

switchPos :: (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n

Instances

(Pos x, Digits xs) => Positive (Pos x xs)

class Integer n => Negative n where

Methods

switchNeg :: (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> f n

Instances

(Pos x, Digits xs) => Negative (Neg x xs)

reifyIntegral :: Integer -> (forall s. Integer s => Proxy s -> w) -> w

reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> a) -> Maybe a

reifyPositive :: Integer -> (forall s. Positive s => Proxy s -> a) -> Maybe a

reifyNegative :: Integer -> (forall s. Negative s => Proxy s -> a) -> Maybe a

reifyPos :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Pos x xs) -> a) -> Maybe a

reifyNeg :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Neg x xs) -> a) -> Maybe a

class Digits xs where

Methods

switchDigits :: f EndDesc -> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f xs

Instances

Digits EndDesc

(C xh, Digits xl) => Digits ((:>) xh xl)

type family x :+: y

Instances

type Zero :+: y = y

type (Pos x xs) :+: Zero = Pos x xs

type (Neg x xs) :+: Zero = Neg x xs

type (Pos x xs) :+: (Neg y ys)

type (Pos x xs) :+: (Pos y ys)

type (Neg x xs) :+: (Pos y ys)

type (Neg x xs) :+: (Neg y ys)

type (:-:) x y = x :+: Negate y

type family x :*: y

Instances

type Zero :*: x = Zero

type (Pos x xs) :*: Zero = Zero

type (Neg x xs) :*: Zero = Zero

type (Pos x xs) :*: (Neg y ys)

type (Pos x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Pos y ys)

type (Neg x xs) :*: (Neg y ys)

type family Pred x

Instances

type Pred Zero = Neg Dec1 EndDesc

type Pred (Pos x xs)

type Pred (Neg x xs)

type family Succ x

Instances

type Succ Zero

type Succ (Pos x xs)

type Succ (Neg x xs)

type family Compare x y

Instances

type Compare Zero Zero = EQ

type Compare Zero (Pos y ys) = LT

type Compare Zero (Neg y ys) = GT

type Compare (Pos x xs) Zero = GT

type Compare (Neg x xs) Zero = LT

type Compare (Pos x xs) (Neg y ys) = GT

type Compare (Pos x xs) (Pos y ys)

type Compare (Neg x xs) (Pos y ys) = LT

type Compare (Neg x xs) (Neg y ys)

type family IsEven x

Instances

type IsEven Zero = True

type IsEven (Pos x xs)

type IsEven (Neg x xs)

type family Pow2 x

Instances

type Pow2 Zero

type Pow2 (Pos x xs)

type family Log2Ceil x

Instances

type Log2Ceil (Pos x xs)

class x :<: y

Instances

Zero :<: (Pos y ys)

(:<:) x y => (Dec x) :<: (Dec y)

(Neg x xs) :<: Zero

(~) * (ComparePos x xs y ys) LT => (Pos x xs) :<: (Pos y ys)

(~) * (ComparePos x xs y ys) GT => (Neg x xs) :<: (Neg y ys)

(Neg x xs) :<: (Pos y ys)

class x :<=: y

Instances

Zero :<=: Zero

Zero :<=: (Pos y ys)

(:<=:) x y => (Dec x) :<=: (Dec y)

(Neg x xs) :<=: Zero

(~) * (GreaterPos x xs y ys) False => (Pos x xs) :<=: (Pos y ys)

(~) * (GreaterPos y ys x xs) False => (Neg x xs) :<=: (Neg y ys)

(Neg x xs) :<=: (Pos y ys)

class x :==: y

Instances

Zero :==: Zero

(:==:) x y => (Dec x) :==: (Dec y)

(~) * (ComparePos x xs y ys) EQ => (Pos x xs) :==: (Pos y ys)

(~) * (ComparePos x xs y ys) EQ => (Neg x xs) :==: (Neg y ys)

class x :>: y

Instances

Zero :>: (Neg y ys)

(:>:) x y => (Dec x) :>: (Dec y)

(Pos x xs) :>: Zero

(~) * (ComparePos x xs y ys) GT => (Pos x xs) :>: (Pos y ys)

(Pos x xs) :>: (Neg y ys)

(~) * (ComparePos x xs y ys) LT => (Neg x xs) :>: (Neg y ys)

class x :>=: y

Instances

Zero :>=: Zero

Zero :>=: (Neg y ys)

(:>=:) x y => (Dec x) :>=: (Dec y)

(Pos x xs) :>=: Zero

(~) * (GreaterPos y ys x xs) False => (Pos x xs) :>=: (Pos y ys)

(Pos x xs) :>=: (Neg y ys)

(~) * (GreaterPos x xs y ys) False => (Neg x xs) :>=: (Neg y ys)

class x :/=: y

Instances

Zero :/=: (Pos y ys)

Zero :/=: (Neg y ys)

(:/=:) x y => (Dec x) :/=: (Dec y)

(Pos x xs) :/=: Zero

(Neg x xs) :/=: Zero

(~) * (IsEQ (ComparePos x xs y ys)) False => (Pos x xs) :/=: (Pos y ys)

(Pos x xs) :/=: (Neg y ys)

(~) * (IsEQ (ComparePos x xs y ys)) False => (Neg x xs) :/=: (Neg y ys)

(Neg x xs) :/=: (Pos y ys)

type family FromUnary n

Instances

type FromUnary Zero = Zero

type FromUnary (Succ n) = Succ (FromUnary n)

type family ToUnary n

Instances

type ToUnary Zero = Zero

type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs

type family ToUnaryAcc m n

Instances

type ToUnaryAcc m EndDesc = m

type ToUnaryAcc m ((:>) x xs) = ToUnaryAcc (UnaryAcc m x) xs

type UnaryAcc m x = ToUnary x :+: (m :*: U10)