Data.Description.Regular

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

data Desc : (Type -> Type) -> Type

  Description of regular functors
  @ p stores additional data for constant types
      e.g. the fact they are enumerable

Totality: total
Visibility: public export
Constructors:

Zero : Desc p

  The code for the empty type

One : Desc p

  The code for the unit type

Id : Desc p

  The code for the identity functor

Const : (0 s : Type) -> p s -> Desc p

  The code for the constant functor

(*) : Desc p -> Desc p -> Desc p

  The code for the product of functors

(+) : Desc p -> Desc p -> Desc p

  The code for the sum of functors

0 Elem : Desc p -> Type -> Type

  Computing the meaning of a description as a functor

Totality: total
Visibility: public export

map : (d : Desc p) -> (a -> b) -> Elem d a -> Elem d b

  Elem does decode to functors

Totality: total
Visibility: export

data Fix : Desc p -> Type

  A regular type is obtained by taking the fixpoint of
  the decoding of a description.
  Unfortunately Idris 2 does not currently detect that this definition
  is total because we do not track positivity in function arguments

Totality: total
Visibility: public export
Constructor: 

MkFix : assert_total (Elem d (Fix d)) -> Fix d

fold : (Elem d x -> x) -> Fix d -> x

  Fix is an initial algebra so we get the fold

Totality: total
Visibility: export

record (~>) : (d : Desc p) -> (Fix d -> Type) -> Type

  A memo trie is a coinductive structure

Totality: total
Visibility: export
Constructor: 

MkMemo : assert_total (Memo d (\x => Inf (d ~> x)) (b . MkFix)) -> d ~> b

Projection: 

.getMemo : d ~> b -> assert_total (Memo d (\x => Inf (d ~> x)) (b . MkFix))

Fixity Declaration: infixr operator, level 0

trie : ((x : Fix d) -> b x) -> d ~> b

Totality: total
Visibility: export

untrie : d ~> b -> (x : Fix d) -> b x

Totality: total
Visibility: export

memo : (0 b : (Fix d -> Type)) -> ((x : Fix d) -> b x) -> (x : Fix d) -> b x

Totality: total
Visibility: export