Data.Enumerate

(source)

The content of this module is based on the paper
A Completely Unique Account of Enumeration
by Cas van der Rest, and Wouter Swierstra
https://doi.org/10.1145/3547636

Definitions

record Enumerator : Type -> Type -> Type

  An (a,b)-enumerator is an enumerator for values of type b provided
  that we already know how to enumerate subterms of type a

Totality: total
Visibility: export
Constructor:

MkEnumerator : (List a -> List b) -> Enumerator a b

Projection:

.runEnumerator : Enumerator a b -> List a -> List b

Hints:

Alternative (Enumerator a)
Applicative (Enumerator a)
Functor (Enumerator a)
Monad (Enumerator a)

pairWith : (b -> c -> d) -> Enumerator a b -> Enumerator a c -> Enumerator a d

  This interleaving is fair, unlike one defined using concatMap.
  Cf. paper for definition of fairness

Totality: total
Visibility: export

pair : Enumerator a b -> Enumerator a c -> Enumerator a (b, c)

Totality: total
Visibility: export

const : List b -> Enumerator a b

  Like `pure` but returns more than one result

Totality: total
Visibility: export

rec : Enumerator a a

  The construction of recursive substructures is memoised by
  simply passing the result of the recursive call

Totality: total
Visibility: export

sized : Enumerator a a -> Nat -> List a

  Assuming that the enumerator is building one layer of term,
  sized e n will produce a list of values of depth n

Totality: total
Visibility: export

stream : Enumerator a a -> Stream (List a)

  Assuming that the enumerator is building one layer of term,
  stream e will produce a list of increasingly deep values

Totality: total
Visibility: export

regular : (d : Desc List) -> Enumerator (Fix d) (Fix d)

Totality: total
Visibility: export