Data.Cardinal

Documentation

data Zero

Instances

Show Zero

Generic Zero

Cardinal Zero

Cardinal a => Prod a Zero

Cardinal a => Sum a Zero

DropList Zero Nil

TakeList Zero Nil

HeadTail l => Component l Zero

DropList Zero l => DropList Zero (:|: e l)

TakeList Zero l => TakeList Zero (:|: e l)

(Ordinal i1, Ordinal i2, Sum i1 i2, MultiIndex is) => MultiIndexConcat Zero (:|: i1 is) (:|: i2 is)

class Cardinal a where

Cardinal number as a type. The associated data type Succ a provides the next cardinal type. The method fromCardinal provides a numeric representation of the cardinal number; it should be independent on the argument and work on undefined.

Associated Types

data Succ a

Methods

fromCardinal :: Num i => a -> i

Instances

Cardinal Zero

Cardinal a => Cardinal (Succ a)

type C0 = Zero

type C1 = Succ C0

type C2 = Succ C1

type C3 = Succ C2

type C4 = Succ C3

type C5 = Succ C4

type C6 = Succ C5

type C7 = Succ C6

type C8 = Succ C7

type C9 = Succ C8

type C10 = Succ C9

class Cardinal (Card a) => Cardinality a

The cardinality of a type is defined by its Cardinal type Card a.

Associated Types

type Card a

Instances

Cardinality One

Cardinality Nil

Cardinality n => Cardinality (Succ n)

(Cardinality e, Cardinality l, Cardinal (:*: (Card e) (Card l))) => Cardinality (:|: e l)

card :: (Cardinality a, Num i) => a -> i

The numeric cardinality of a type. card is independent on its argument.

class GCardinality a

Associated Types

type GCard a

Instances

GCardinality (V1 p)

GCardinality (U1 p)

Cardinality a => GCardinality (K1 i a p)

(GCardinality (f p), GCardinality (g p)) => GCardinality (:+: f g p)

(GCardinality (f p), GCardinality (g p)) => GCardinality (:*: f g p)

GCardinality (f p) => GCardinality (M1 i c f p)

module Data.TypeAlgebra