Safe Haskell | None |
---|---|

Language | Haskell2010 |

the cardinality of a finite type, at the type-level.

- class Finite a where
- type Cardinality a :: Nat

- type family GCardinality f :: Nat
- reifyCardinality :: forall a proxy. KnownNat (Cardinality a) => proxy a -> Natural
- type CardinalityWithin n a = IsCardinalityWithin n a ~ True
- type IsCardinalityWithin n a = Cardinality a <=? n

# Documentation

a type is finite, i.e. has a bounded size.

laws:

consistent with Enumerate.Enumerable:

`cardinality`

=`reifyCardinality`

i.e. the value-level (a

`Natural`

) matches the type-level (a`Nat`

)

e.g.

`>>>`

2`reifyCardinality ([]::[Bool])`

type Cardinality a :: Nat Source

type family GCardinality f :: Nat Source

type GCardinality V1 = 0 Source | |

type GCardinality U1 = 1 Source | |

type GCardinality (K1 i a) = Cardinality a Source | |

type GCardinality ((:+:) f g) = (+) (GCardinality f) (GCardinality g) Source | |

type GCardinality ((:*:) f g) = * (GCardinality f) (GCardinality g) Source | |

type GCardinality (M1 i t f) = GCardinality f Source |

reifyCardinality :: forall a proxy. KnownNat (Cardinality a) => proxy a -> Natural Source

`>>>`

2`reifyCardinality ([]::[Bool])`

type CardinalityWithin n a = IsCardinalityWithin n a ~ True Source

typechecks only when the constraint is satisifed.

a constaint.

type IsCardinalityWithin n a = Cardinality a <=? n Source

a predicate, inclusive.

> type CardinalityWithinAMillion a = CardinalityWithin 1000000 a > :kind! CardinalityWithinAMillion Bool True > :kind! CardinalityWithinAMillion Char False