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

Portabilitynon-portable (type families, requires ghc >= 6.9)



Type-level numerical operations using type families.



data ds :. d Source


(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 IntegerT x whereSource


fromIntegerT :: Num y => x -> ySource


IntegerT' x => IntegerT (Dec x) 

class IntegerT x => NaturalT x Source


class IntegerT x => PositiveT x Source


class IntegerT x => NegativeT x Source