tfp-1.0: Type-level integers, booleans, lists using type families

Safe HaskellSafe-Inferred
LanguageHaskell2010

Type.Data.Num.Unary

Synopsis

Documentation

data Unary Source

Representation name for unary type level numbers.

Instances

data Un x Source

Instances

Natural n => Integer (Un n) 
type Repr (Un n) = Unary 
type (Un x) :*: (Un y) = Un ((:*:) x y) 
type (Un x) :+: (Un y) = Un ((:+:) x y) 

data Zero Source

Instances

Natural Zero 
type FromUnary Zero = Zero 
type x :*: Zero = Zero 
type x :+: Zero = x 

data Succ x Source

Instances

Natural n => Positive (Succ n) 
Natural n => Natural (Succ n) 
type x :*: (Succ y) = (:+:) x ((:*:) x y) 
type x :+: (Succ y) = Succ ((:+:) x y) 
type FromUnary (Succ n) = Succ (FromUnary n) 

zero :: Proxy Zero Source

succ :: Proxy n -> Proxy (Succ n) Source

newtype Singleton n Source

Constructors

Singleton Integer 

singleton :: Natural n => Singleton n Source

singletonFromProxy :: Natural n => Proxy n -> Singleton n Source

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

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

class Natural n where Source

Methods

switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f n Source

Instances

class Natural n => Positive n where Source

Methods

switchPos :: (forall m. Natural m => f (Succ m)) -> f n Source

Instances

Natural n => Positive (Succ n) 

type family x :+: y Source

Instances

type x :+: Zero = x 
type x :+: (Succ y) = Succ ((:+:) x y) 

type family x :*: y Source

Instances

type x :*: Zero = Zero 
type x :*: (Succ y) = (:+:) x ((:*:) x y)