A coenumeration is a function from values to finite or countably infinite sets, canonically represented by non-negative integers less than its cardinality.

Alternatively, a coenumeration can be thought of as a classification of values into finite or countably infinite classes, with each class labelled with integers.

CoEnumeration is an instance of the following type classes:

• Contravariant (you can change the type of base values contravariantly)

• Divisible (representing Cartesian product of finite number of coenumerations)

  • Binary cartesian product (><)
  • Coenumeration onto singleton set as an unit (unit)

• Decidable (representing disjoint union of finite number of coenumerations)

  • Binary disjoint union (<+>)

  • Coenumeration of uninhabited type Void. It's not exported directly, but only through a method of the class

    lose :: Decidable f => (a -> Void) -> f Void

    or

    lost :: Decidable f => f Void.

Get the cardinality of a coenumeration. Under "classification" interpretation, it is the cardinality of the set of classes.

Compute the index of a particular value.

Returns if the the cardinality of coenumeration is finite.

Constructs a coenumeration.

To construct valid coenumeration by unsafeMkCoEnumeration n f, for all x :: a, it must satisfy (Finite (f x) < n).

This functions does not (and never could) check the validity of its arguments.

An index into an enumeration.

The cardinality of a countable set: either a specific finite natural number, or countably infinite.

Coenumeration to the singleton set.

>>> card unit
Finite 1
>>> locate unit True
0
>>> locate unit (3 :: Int)
0
>>> locate unit (cos :: Float -> Float)
0

lost = lose id

An inverse of forward boundedEnum

nat is an inverse of forward enumeration nat.

For a negative integer x which nat doesn't enumerate, locate nat x returns the same index to the absolute value of x, i.e. locate nat x == locate nat (abs x).

>>> locate nat <$> [-3 .. 3]
[3,2,1,0,1,2,3]

int is the inverse of forward enumeration int, which is all integers ordered as the sequence 0, 1, -1, 2, -2, ...

>>> locate int <$> [1, 2, 3, 4, 5]
[1,3,5,7,9]
>>> locate int <$> [0, -1 .. -5]
[0,2,4,6,8,10]

cw is an inverse of forward enumeration cw.

Because cw only enumerates positive Rational values, locate cw x for zero or less rational number x could be arbitrary.

This implementation chose locate cw x = 33448095 for all x <= 0, which is the index of 765 % 4321, rather than returning undefined.

>>> locate cw <$> [1 % 1, 1 % 2, 2 % 1, 1 % 3, 3 % 2]
[0,1,2,3,4]
>>> locate cw (765 % 4321)
33448095
>>> locate cw 0
33448095

rat is the inverse of forward enumeration rat.

>>> let xs = E.enumerate . E.takeE 6 $ E.rat
>>> (xs, locate rat <$> xs)
([0 % 1,1 % 1,(-1) % 1,1 % 2,(-1) % 2,2 % 1],[0,1,2,3,4,5])
>>> locate rat (E.select E.rat 1000)
1000

>>> locate (takeC 3 nat) <$> [0..5]
[0,1,2,2,2,2]

>>> locate (dropC 3 nat) <$> [0..5]
[0,0,0,0,1,2]

>>> locate (modulo 3) <$> [0..7]
[0,1,2,0,1,2,0,1]
>>> locate (modulo 3) (-4)
2

overlayC a b combines two coenumerations in parallel, sharing indices of two coenumerations.

The resulting coenumeration has cardinality of the larger of the two arguments.

Sets the cardinality of given coenumeration to Infinite

Cartesian product of coenumeration, made to be an inverse of cartesian product of enumeration (><).

>>> let a  = E.finite 3 E.>< (E.boundedEnum @Bool)
>>> let a' = modulo 3     >< boundedEnum @Bool
>>> (E.enumerate a, locate a' <$> E.enumerate a)
([(0,False),(0,True),(1,False),(1,True),(2,False),(2,True)],[0,1,2,3,4,5])

This operation is not associative if and only if one of arguments is not finite.

Sum, or disjoint union, of two coenumerations.

It corresponds to disjoint union of enumerations eitherOf.

Its type can't be CoEnumeration a -> CoEnumeration a -> CoEnumeration a, like Enumeration which is covariant functor, because CoEnumeration is Contravariant functor.

>>> let a  = E.finite 3 `E.eitherOf` (E.boundedEnum @Bool)
>>> let a' = modulo 3    <+>          boundedEnum @Bool
>>> (E.enumerate a, locate a' <$> E.enumerate a)
([Left 0,Left 1,Left 2,Right False,Right True],[0,1,2,3,4])

This operation is not associative if and only if one of arguments is not finite.

The inverse of forward maybeOf

Synonym of (<+>)

Coenumerate all possible finite lists using given coenumeration.

If a coenumeration a is the inverse of enumeration b, listOf a is the inverse of forward enumeration listOf b.

>>> E.enumerate . E.takeE 6 $ E.listOf E.nat
[[],[0],[0,0],[1],[0,0,0],[1,0]]
>>> locate (listOf nat) <$> [[],[0],[0,0],[1],[0,0,0],[1,0]]
[0,1,2,3,4,5]
>>> E.select (E.listOf E.nat) 1000000
[1008,26,0]
>>> locate (listOf nat) [1008,26,0]
1000000

An inverse of finiteSubsetOf.

Given a coenumeration of a, make a coenumeration of finite sets of a, by ignoring order and repetition from [a].

>>> as = take 11 . E.enumerate $ E.finiteSubsetOf E.nat
>>> (as, locate (finiteSubsetOf nat) <$> as)
([[],[0],[1],[0,1],[2],[0,2],[1,2],[0,1,2],[3],[0,3],[1,3]],[0,1,2,3,4,5,6,7,8,9,10])

An inverse of finiteEnumerationOf.

Given a coenumeration of a, make a coenumeration of function from finite sets to a.

Ideally, its type should be the following dependent type

{n :: Integer} -> CoEnumeration a -> CoEnumeration ({k :: Integer | k < n} -> a)

>>> let as = E.finiteEnumerationOf 3 (E.takeE 2 E.nat)
>>> map E.enumerate $ E.enumerate as
[[0,0,0],[0,0,1],[0,1,0],[0,1,1],[1,0,0],[1,0,1],[1,1,0],[1,1,1]]
>>> let inv_as = finiteFunctionOf 3 (takeC 2 nat)
>>> locate inv_as (E.select (E.finiteList [0,1,1]))
3