Data.SOP.POP

Definitions

data POP_ : (k : Type) -> (k -> Type) -> List (List k) -> Type

  A product of products.
  
  The elements of the inner products are
  applications of the parameter f. The type POP is indexed by the list of lists
  that determines the lengths of both the outer and all the inner products, as
  well as the types of all the elements of the inner products.
  
  A POP is reminiscent of a two-dimensional table (but the inner lists can all be
  of different length). In the context of the SOP approach to
  generic programming, a POP is useful to represent information
  that is available for all arguments of all constructors of a datatype.

Totality: total
Visibility: public export
Constructor: 

MkPOP : NP_ (List k) (NP_ k f) kss -> POP_ k f kss

Hints:

POP (DecEq . f) kss => DecEq (POP_ k f kss)

POP (Eq . f) kss => Eq (POP_ k f kss)

HAp k (List (List k)) (POP_ k) (POP_ k)

HAp k (List (List k)) (POP_ k) (SOP_ k)

HCollapse k (List (List k)) (POP_ k) (List . List)

HFold k (List (List k)) (POP_ k)

HFunctor k (List (List k)) (POP_ k)

HPure k (List (List k)) (POP_ k)

HSequence k (List (List k)) (POP_ k)

POP (Monoid . f) kss => Monoid (POP_ k f kss)

POP_ k (c . f) kss -> (NP_ k (c . f) ks => c (NP_ k f ks)) => NP_ (List k) (c . NP_ k f) kss

POP (Ord . f) kss => Ord (POP_ k f kss)

POP (Semigroup . f) kss => Semigroup (POP_ k f kss)

POP (Show . f) kss => Show (POP_ k f kss)

POP : (k -> Type) -> List (List k) -> Type

  Type alias for `POP_` with type parameter `k` being
  implicit. This reflects the kind-polymorphic data type
  in Haskell.

Totality: total
Visibility: public export

unPOP : POP_ k f kss -> NP_ (List k) (NP_ k f) kss

Totality: total
Visibility: public export

mapPOP : (f a -> g a) -> POP f kss -> POP g kss

  Specialiced version of `hmap`

Totality: total
Visibility: public export

purePOP : f a -> POP f kss

  Specialization of `hpure`.

Totality: total
Visibility: public export

hapPOP : POP (\a => f a -> g a) kss -> POP f kss -> POP g kss

  Specialization of `hap`.

Totality: total
Visibility: public export

foldlPOP : (acc -> el -> acc) -> acc -> POP (K el) kss -> acc

  Specialization of `hfoldl`

Totality: total
Visibility: public export

foldrPOP : (el -> Lazy acc -> acc) -> Lazy acc -> POP (K el) kss -> acc

  Specialization of `hfoldr`

Totality: total
Visibility: public export

sequencePOP : Applicative g => POP (\a => g (f a)) kss -> g (POP f kss)

  Specialization of `hsequence`

Totality: total
Visibility: public export

collapsePOP : POP (K a) kss -> List (List a)

  Specialization of `hcollapse`

Totality: total
Visibility: public export

ordToEqPOP : POP (Ord . f) kss -> POP (Eq . f) kss

  This is needed to implement `Ord` below.

Totality: total
Visibility: public export

monoidToSemigroupPOP : POP (Monoid . f) kss -> POP (Semigroup . f) kss

  This is needed to implement `Monoid` below.

Totality: total
Visibility: public export

popToNP : POP_ k (c . f) kss -> (NP_ k (c . f) ks => c (NP_ k f ks)) => NP_ (List k) (c . NP_ k f) kss

  Converts a POP of constraints to an n-ary sum
  holding constrains about the inner n-ary sum.
  
  Example : POP Eq typess -> NP (Eq . NP I) typess
  
  In the example above, we convert a POP of `Eq` instances
  into an n-ary sum of Eq instances of the inner products.
  This allows us to for instance implent `Eq (POP f kss) ` below
  via a direct call to (==) specialized to Eq (NP (NP f) kss).

Totality: total
Visibility: public export