Data.Cardinal

Documentation

data Zero

Instances

Show Zero

Cardinal Zero

Cardinal a => Prod a Zero

Cardinal a => Sum a Zero

DropList Zero Nil

TakeList Zero Nil

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

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.

module Data.TypeAlgebra