sized-vector-0.0.1.0: Size-parameterized vector types and functions.

Data.Type.Natural

Description

Type level peano natural number, some arithmetic functions and their singletons.

Synopsis

Natural numbers and its singleton type

data Nat Source

Peano natural numbers. It will be promoted to the type-level natural number.

Constructors

 Z S Nat

Instances

 Eq Nat Num Nat Ord Nat Show Nat

data SNat n whereSource

Singleton type for `Nat`. When constructing data, use smart constructors such as `sZ` and `sS`.

Constructors

 SZ :: SNat Z SS :: SNat n -> SNat (S n)

Smart constructors

The smart constructor for `SZ`.

sS :: SNat n -> SNat (S n)Source

The smart constructor for `SS n`.

Arithmetic functions and thir singletons.

min :: Nat -> Nat -> NatSource

Minimum function.

type family Min n m :: NatSource

Type-level minimum function.

sMin :: SNat n -> SNat m -> SNat (Min n m)Source

Singleton function for minimum function.

max :: Nat -> Nat -> NatSource

Maximum function.

type family Max n m :: NatSource

Type-level maximum function.

sMax :: SNat n -> SNat m -> SNat (Max n m)Source

Singleton function for maximum.

type family n :+: m :: NatSource

(%+) :: SNat n -> SNat m -> SNat (n :+: m)Source

type family n :*: m :: NatSource

Type-level multiplication.

(%*) :: SNat n -> SNat m -> SNat (n :*: m)Source

Multiplication for singleton numbers.

type family n :-: m :: NatSource

(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)Source

Type-level predicate & judgements

data Leq n m whereSource

Constructors

 ZeroLeq :: SNat m -> Leq Zero m SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

class n :<= m Source

Comparison via type-class.

Instances

 Z :<= n :<= n m => (S n) :<= (S m)

type family n :<<= m :: BoolSource

Comparison function

boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n mSource

boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n mSource

Type-classes for singletons

class Sing n whereSource

Singleton type-class. This class will be removed soon after singletons package available for the latest Haskell Paltform.

Methods

Automatically compute singletons.

Instances

 Sing Z Sing n => Sing (S n)

data SingInstance a whereSource

Witness for `Sing` instance. This type will be removed soon after singletons package available for the latest Haskell Paltform.

Constructors

 SingInstance :: Sing a => SingInstance a

Get witness for singleton integers. This function will be removed soon after singletons package available for the latest Haskell Paltform.

Conversion functions

natToInt :: Integral n => Nat -> nSource

Convert `Nat` into normal integers.

intToNat :: (Integral a, Ord a) => a -> NatSource

Convert integral numbers into `Nat`

sNatToInt :: Num n => SNat x -> nSource

Convert 'SNat n' into normal integers.

Useful type synonyms and constructors

type Zero = ZSource

type Two = S OneSource

type N0 = ZSource

type N1 = OneSource

type N2 = TwoSource

type N4 = FourSource

type N5 = FiveSource

type N6 = SixSource

type N9 = NineSource

type N10 = TenSource