Safe Haskell	None
Language	Haskell2010

Enumerate.Cardinality

Description

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

Synopsis

Documentation

class Finite a Source

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.

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

Associated Types

type Cardinality a :: Nat Source

Instances

Finite Bool Source	2
Finite Char Source	1114112
Finite Int8 Source	2^8
Finite Int16 Source	2^16
Finite Ordering Source	3
Finite Word8 Source	2^8
Finite Word16 Source	2^16
Finite () Source	1
Finite Void Source	0
Finite a => Finite (Maybe a) Source	1 + a
Finite a => Finite (Set a) Source	2^a
(Finite a, Finite b) => Finite (a -> b) Source	b^a
(Finite a, Finite b) => Finite (Either a b) Source	a + b
(Finite a, Finite b) => Finite (a, b) Source	a*b
Finite (Proxy * a) Source
(Finite a, Finite b, Finite c) => Finite (a, b, c) Source	abc
Finite (Rec * f ([] *)) Source
(Finite (f a), Finite (Rec * f as)) => Finite (Rec * f ((:) * a as)) Source	the cardinality is a product of cardinalities.
(Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d) Source	abc*d
(Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e) Source	abcde
(Finite a, Finite b, Finite c, Finite d, Finite e, Finite f) => Finite (a, b, c, d, e, f) Source	abcde*f
(Finite a, Finite b, Finite c, Finite d, Finite e, Finite f, Finite g) => Finite (a, b, c, d, e, f, g) Source	abcdefg

type family GCardinality f :: Nat Source

Instances

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

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

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