tfp-0.5: Type-level programming library using type families

Portabilitynon-portable (type families, requires ghc >= 6.9)
Stabilityexperimental
Maintainerpgavin@gmail.com
Safe HaskellNone

Types.Data.Num.Ops

Description

Type-level numerical operations using type families.

Synopsis

Documentation

data ds :. d Source

Instances

(Show ds, Show d) => Show (:. ds d) 
IntegerT' xh => IntegerT' (:. xh Dec9) 
IntegerT' xh => IntegerT' (:. xh Dec8) 
IntegerT' xh => IntegerT' (:. xh Dec7) 
IntegerT' xh => IntegerT' (:. xh Dec6) 
IntegerT' xh => IntegerT' (:. xh Dec5) 
IntegerT' xh => IntegerT' (:. xh Dec4) 
IntegerT' xh => IntegerT' (:. xh Dec3) 
IntegerT' xh => IntegerT' (:. xh Dec2) 
IntegerT' xh => IntegerT' (:. xh Dec1) 
IntegerT' xh => IntegerT' (:. xh Dec0) 

type family Neg x Source

Neg x evaluates to the additive inverse of (i.e., minus) x.

negT :: x -> Neg xSource

type family IsPositive x Source

type family IsZero x Source

type family IsNegative x Source

type family Succ x Source

succT :: x -> Succ xSource

type family Pred x Source

predT :: x -> Pred xSource

type family IsEven x Source

type family IsOdd x Source

type family x :+: y Source

addT :: x -> y -> x :+: ySource

type family x :-: y Source

subT :: x -> y -> x :-: ySource

type family x :*: y Source

mulT :: x -> y -> x :*: ySource

type family Mul2 x Source

mul2T :: x -> Mul2 xSource

type family Pow2 x Source

pow2T :: x -> Pow2 xSource

type family DivMod x y Source

divModT :: x -> y -> DivMod x ySource

type family Div x y Source

divT :: x -> y -> Div x ySource

type family Mod x y Source

modT :: x -> y -> Mod x ySource

type family Div2 x Source

div2T :: x -> Div2 xSource

type family Fac x Source

facT :: x -> Fac xSource

class IntegerR r whereSource

Methods

reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> aSource

Instances

class IntegerR (Repr x) => IntegerT x whereSource

Associated Types

type Repr x Source

Methods

fromIntegerT :: Num y => x -> ySource

Instances

IntegerT x => IntegerT (AssertNeg x) 
IntegerT x => IntegerT (AssertPos x) 
IntegerT' x => IntegerT (Dec x) 

class IntegerT x => NaturalT x Source

Instances

(IntegerT x, ~ * (IsNegative x) False) => NaturalT x 

class IntegerT x => PositiveT x Source

Instances

(IntegerT x, ~ * (IsPositive x) True) => PositiveT x 

class IntegerT x => NegativeT x Source

Instances

(IntegerT x, ~ * (IsNegative x) True) => NegativeT x 

reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe aSource

reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe aSource