Data.SOP.SOP

Definitions

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

  A sum of products.
  
  The elements of the (inner) products
  are applications of the parameter f. The type SOP_ is indexed by the list of
  lists that determines the sizes of both the (outer) sum and all the (inner)
  products, as well as the types of all the elements of the inner products.
  
  A SOP I reflects the structure of a normal Idris datatype. The sum structure
  represents the choice between the different constructors, the product structure
  represents the arguments of each constructor.

Totality: total
Visibility: public export
Constructor: 

MkSOP : NS_ (List k) (NP_ k f) kss -> SOP_ k f kss

Hints:

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

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

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

HCollapse k (List (List k)) (SOP_ k) List

HFold k (List (List k)) (SOP_ k)

HFunctor k (List (List k)) (SOP_ k)

HSequence k (List (List k)) (SOP_ k)

POP (Monoid . f) [ks] => Monoid (SOP_ k f [ks])

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

POP (Semigroup . f) [ks] => Semigroup (SOP_ k f [ks])

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

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

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

Totality: total
Visibility: public export

unSOP : SOP_ k f kss -> NS_ (List k) (NP_ k f) kss

Totality: total
Visibility: public export

mapSOP : (f a -> g a) -> SOP f kss -> SOP g kss

  Specialiced version of `hmap`

Totality: total
Visibility: public export

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

  Specialization of `hap`

Totality: total
Visibility: public export

foldlSOP : (acc -> el -> acc) -> acc -> SOP (K el) kss -> acc

  Specialization of `hfoldl`

Totality: total
Visibility: public export

foldrSOP : (el -> Lazy acc -> acc) -> Lazy acc -> SOP (K el) kss -> acc

  Specialization of `hfoldr`

Totality: total
Visibility: public export

sequenceSOP : Applicative g => SOP (\a => g (f a)) kss -> g (SOP f kss)

  Specialization of `hsequence`

Totality: total
Visibility: public export

collapseSOP : SOP (K a) kss -> List a

  Specialization of `hcollapse`

Totality: total
Visibility: public export

0 InjectionSOP : (k -> Type) -> List (List k) -> List k -> Type

  An injection into an n-ary sum of products takes an n-ary product of
  the correct type and wraps it in one of the sum's possible choices.

Totality: total
Visibility: public export

injectionsSOP : NP_ (List k) (InjectionSOP f kss) kss

  The set of injections into an n-ary sum `NS f ks` can
  be wrapped in a corresponding n-ary product.

Totality: total
Visibility: public export

apInjsPOP_ : POP f kss -> NP (K (SOP f kss)) kss

  Applies all injections to a product of products of values.
  
  This is not implemented in terms of `injectionsSOP` for the
  following reason: Since we have access to the structure
  of the product of products and thus `kss`, we do not need a
  runtime reference of `kss`. Therefore, when applying
  injections to a product of products, prefer this function
  over a combination involving `injectionsSOP`.

Totality: total
Visibility: public export

apInjsPOP : POP f kss -> List (SOP f kss)

  Alias for `collapseNP . apInjsPOP_`

Totality: total
Visibility: public export

injectSOP : NP f ks -> Elem ks kss => SOP f kss

  Injects a product into an n-ary sum of products.

Totality: total
Visibility: public export

extractSOP : (0 ks : List k) -> SOP f kss -> Elem ks kss => Maybe (NP f ks)

  Tries to extract a product of the given type from an
  n-ary sum of products.

Totality: total
Visibility: public export