Data.SOP.Interfaces

This module provides interfaces similar to `Applicative`
and `Traversable` for heterogeneous container types.
We distinguish between two types of containers: Product
types hold all their values at once, while sum types
represent a choice: A generalization of `Either`.

The core data types in this library are indexed over a
container (typically a List or List of Lists) of values
of type `k` plus a type-level function `f` of type `k -> Type`.
The values of the container index together with `f` determine
the types of values at each position in the
heterogeneous product or sum, while the shape of container
indices mirror the shape of the corresponding product types.

The interfaces in this module allow us to create
hetereogeneous containers from sufficiently general functions
(`HPure`), use unary functions to change the context of
values in a heterogeneous container (`HFunctor`),
collapse heterogeneous containers into a single value (`HFoldable`)
and run an effectful computation over all values in
a heterogeneous container (`HSequence`).

In addition, `HFunctor` can be generalized to arbitrary
n-ary functions (`HAp`). However, this case is special in that only
the last argument of such a function can be a sum type
while all other arguments have to be product types.
This makes sense, since when combining values of two sum types,
we typically cannot guarantee that the values point at
same choice and are therefore compatible.

Implementation notes:

For many of the functions in this module, there is a constrained
version taking an implicit heterogeneous product holding
the desired implementations. Since Idris2 uses the same
mechanism for resolving interface constraints and auto implicits,
we do not need an additional structure or interface
for these constraints.
The disadvantage of this is, that we more often have to explicitly
pattern match on these constraint products in order for Idris2
to know where to look for implementations.

Definitions

HCont : Type -> Type -> Type

  A heterogeneous container indexed over a container type `l`
  holding values of type `k`.

Totality: total
Visibility: public export

interface HPure : (k : Type) -> (l : Type) -> HCont k l -> Type

  This interface allows a heterogenous product to be filled
  with values, given a function which produce values of
  every possible type required.
  
  @ k kind of Types in a heterogeneous container's  type level code
  
  @ l kind of container used to describe a heterogeneous containr's type
      level code
  
  @ p the heterogeneous sum or product

Parameters: k, l, p
Methods:

hpure : f a -> p f ks

  Creates a heterogeneous product by using the given functio
  to produce values.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  emptyPerson : Person Maybe
  emptyPerson = hpure Nothing
  ```

Implementations:

HPure k (List k) (NP_ k)

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

hpure : HPure k l p => f a -> p f ks

  Creates a heterogeneous product by using the given functio
  to produce values.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  emptyPerson : Person Maybe
  emptyPerson = hpure Nothing
  ```

Totality: total
Visibility: public export

hempty : Alternative f => HPure Type l p => p f ks

  Alias for `hpure empty`.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  emptyPerson : Person Maybe
  emptyPerson = empty
  ```

Totality: total
Visibility: public export

hconst : HPure k l p => a -> p (K a) ks

  Fills a heterogeneous structure with a constant value
  in the (K a) functor.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  fooPerson : Person (K String)
  fooPerson = hconst "foo"
  ```

Totality: total
Visibility: public export

interface HFunctor : (k : Type) -> (l : Type) -> HCont k l -> Type

  A higher kinded functor allowing us to change the
  wrapper type or context of an n-ary sum or product.
  
  @ k kind of Types in a heterogeneous container's  type level code
  
  @ l kind of container used to describe a heterogeneous containr's type
      level code
  
  @ p the actual heterogeneous container

Parameters: k, l, p
Methods:

hmap : (f a -> g a) -> p f ks -> p g ks

  Maps the given function over all values in a
  heterogeneous container, thus changing the context
  of all of its values.
  
  @ fun maps values in a heterogeneous container to a new context
  
  @ p   the heterogeneous container, over which `fun` is mapped.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  toPersonMaybe : Person I -> Person Maybe
  toPersonMaybe = hmap Just
  ```

Implementations:

HFunctor k (List k) (NS_ k)

HFunctor k (List k) (NP_ k)

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

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

hmap : HFunctor k l p => (f a -> g a) -> p f ks -> p g ks

  Maps the given function over all values in a
  heterogeneous container, thus changing the context
  of all of its values.
  
  @ fun maps values in a heterogeneous container to a new context
  
  @ p   the heterogeneous container, over which `fun` is mapped.
  
  ```idris example
  Person : (f : Type -> Type) -> Type
  Person f = NP f [String,Int]
  
  toPersonMaybe : Person I -> Person Maybe
  toPersonMaybe = hmap Just
  ```

Totality: total
Visibility: public export

hliftA : HFunctor k l p => (f a -> g a) -> p f ks -> p g ks

  Alias for `hmap`

Totality: total
Visibility: public export

hcpure : HFunctor k l p => (0 c : (k -> Type)) -> p c ks => (c a => f a) -> p f ks

  Like `hpure` but using a constrained function for
  generating values. Since Idris is able to provide
  the required constraints
  already wrapped in a container of the correct
  shape, this is actually a derivative of `HFunctor` and not
  `HPure`. This has interesting consequences for sum
  types, for which this function is available as well.
  Since Idris has to choose a value of the sum
  itself, it will use the first possibility it
  can fill with the requested constraints.
  
  In the first example below, Idris generates the value
  `MkSOP (Z ["","",[]])`. However, if the first choice does
  not have a Monoid instance, Idris faithfully chooses the
  next working possibility. In the second example,
  the result is `MkSOP (S (Z [[],[]]))`:
  
  ```idris example
  neutralFoo : SOP I [[String,String,List Int],[Int]]
  neutralFoo = hcpure Monoid neutral
  
  neutralBar : SOP I [[String,Int,List Int],[List String, List Int]]
  neutralBar = hcpure Monoid neutral
  ```
  
  @ c   erased function argument to specify the constraint
        to use
  
  @ fun generates values depending on the availability of
        a constraint

Totality: total
Visibility: public export

interface HAp : (k : Type) -> (l : Type) -> ((k -> Type) -> l -> Type) -> ((k -> Type) -> l -> Type) -> Type

  Like `Applicative`, this interface allows to
  map arbitrary n-ary Rank-2 functions over
  heterogeneous data structures of the same shape.
  However, in order to support products as well as sum types
  all arguments except the last one have to be products
  indexed over the same container as the last argument.
  
  @ k kind of Types in a heterogeneous container's  type level code
  
  @ l kind of container used to describe a heterogeneous containr's type
      level code
  
  @ q heterogeneous product related to `p`. For product types,
      this is the same as `p`, for sum types it is the corresponding
      product type.
  
  @ p the actual heterogeneous container (sum or product)

Parameters: k, l, q, p
Constraints: HFunctor k l q, HFunctor k l p
Methods:

hap : q (\a => f a -> g a) ks -> p f ks -> p g ks

  Higher kinded equivalent to `(<*>)`.
  
  Applies wrapped functions in the product
  container to the corresponding values in the
  second container.
  
  @ q product holding unary Rank-2 functions.
  
  @ p sum or product to whose values the functions in `q` should
      be applied
  
  ```idris example
  hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
  hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])
  ```

Implementations:

HAp k (List k) (NP_ k) (NS_ k)

HAp k (List k) (NP_ k) (NP_ k)

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

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

hap : HAp k l q p => q (\a => f a -> g a) ks -> p f ks -> p g ks

  Higher kinded equivalent to `(<*>)`.
  
  Applies wrapped functions in the product
  container to the corresponding values in the
  second container.
  
  @ q product holding unary Rank-2 functions.
  
  @ p sum or product to whose values the functions in `q` should
      be applied
  
  ```idris example
  hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
  hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])
  ```

Totality: total
Visibility: public export

hliftA2 : HAp k l q p => (f a -> g a -> h a) -> q f ks -> p g ks -> p h ks

  Higher kinded version of `liftA2`.
  This is a generalization of `hliftA` to binary
  functions.

Totality: total
Visibility: public export

hliftA3 : HAp k l q q => HAp k l q p => (f a -> g a -> h a -> i a) -> q f ks -> q g ks -> p h ks -> p i ks

  Higher kinded version of `liftA3`.
  This is a generalization of `hliftA` to ternary
  functions.

Totality: total
Visibility: public export

hliftA4 : HAp k l q q => HAp k l q p => (f a -> g a -> h a -> i a -> j a) -> q f ks -> q g ks -> q h ks -> p i ks -> p j ks

  Higher kinded version of `liftA4`.
  This is a generalization of `hliftA` to quartenary
  functions.

Totality: total
Visibility: public export

hcmap : HAp k l q p => (0 c : (k -> Type)) -> q c ks => (c a => f a -> g a) -> p f ks -> p g ks

  Like `hmap` but uses a constrained function.
  
  @ c   constraint used to convert values
  
  @ fun constrained function for converting values to
        a new context
  
  ```idris example
  showValues : NP I [String,Int] -> NP (K String) [String,Int]
  showValues = hcmap Show show
  ```

Totality: total
Visibility: public export

hcliftA : HAp k l q p => (0 c : (k -> Type)) -> q c ks -> (c a => f a -> g a) -> p f ks -> p g ks

  Alias for `hcmap`

Totality: total
Visibility: public export

hcliftA2 : HAp k l q q => HAp k l q p => (0 c : (k -> Type)) -> q c ks => (c a => f a -> g a -> h a) -> q f ks -> p g ks -> p h ks

  Like `hliftA2` but with a constrained function.

Totality: total
Visibility: public export

hcliftA3 : HAp k l q q => HAp k l q p => (c : (k -> Type)) -> q c ks => (c a => f a -> g a -> h a -> i a) -> q f ks -> q g ks -> p h ks -> p i ks

  Like `hliftA3` but with a constrained function.

Totality: total
Visibility: public export

interface HFold : (k : Type) -> (l : Type) -> HCont k l -> Type

Parameters: k, l, p
Methods:

hfoldl : (acc -> el -> acc) -> acc -> p (K el) ks -> acc

  Strict fold over a heterogeneous sum or product
  parameterized by the constant functor (and thus being actually
  a homogeneous sum or product).

hfoldr : (el -> Lazy acc -> acc) -> Lazy acc -> p (K el) ks -> acc

  Lazy fold over a heterogeneous sum or product
  parameterized by the constant functor (and thus being actually
  a homogeneous sum or product).

Implementations:

HFold k (List k) (NS_ k)

HFold k (List k) (NP_ k)

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

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

hfoldl : HFold k l p => (acc -> el -> acc) -> acc -> p (K el) ks -> acc

  Strict fold over a heterogeneous sum or product
  parameterized by the constant functor (and thus being actually
  a homogeneous sum or product).

Totality: total
Visibility: public export

hfoldr : HFold k l p => (el -> Lazy acc -> acc) -> Lazy acc -> p (K el) ks -> acc

  Lazy fold over a heterogeneous sum or product
  parameterized by the constant functor (and thus being actually
  a homogeneous sum or product).

Totality: total
Visibility: public export

hsize : (HFunctor k l p, HFold k l p) => p f ks -> Nat

  Calculates the size of a heterogeneous container

Totality: total
Visibility: public export

hconcat : (Monoid m, HFold k l p) => p (K m) ks -> m

  Alias for `hfoldl (<+>) neutral`.

Totality: total
Visibility: public export

hconcatMap : Monoid m => HFunctor k l p => HFold k l p => (f a -> m) -> p f ks -> m

  Alias for `hconcat . hmap fun`

Totality: total
Visibility: public export

hcconcatMap : Monoid m => HAp k l q p => HFold k l p => (0 c : (k -> Type)) -> q c ks => (c a => f a -> m) -> p f ks -> m

  Alias for `hconcat . hcmap c fun`

Totality: total
Visibility: public export

hsequence_ : (Applicative g, HFold k l p) => p (K (g ())) ks -> g ()

  Generalization of `sequence_` to heterogeneous containers.
  
  Alias for `hfoldl (*>) (pure ())`.

Totality: total
Visibility: public export

htraverse_ : Applicative g => HFunctor k l p => HFold k l p => (f a -> g ()) -> p f ks -> g ()

  Generalization of `traverse_` to heterogeneous containers.
  
  Alias for `hsequence_ . hmap fun`.

Totality: total
Visibility: public export

hfor_ : (Applicative g, (HFold k l p, HFunctor k l p)) => p f ks -> (f a -> g ()) -> g ()

  Generalization of `for_` to heterogeneous containers.

Totality: total
Visibility: public export

hand : HFold k l p => p (K Bool) ks -> Bool

  Generalization of `and` to heterogeneous containers.

Totality: total
Visibility: public export

htoList : (HFunctor k l p, HFold k l p) => p (K a) ks -> List a

  Generalization of `toList` to heterogeneous containers.

Totality: total
Visibility: export

hor : HFold k l p => p (K Bool) ks -> Bool

  Generalization of `or` to heterogeneous containers.

Totality: total
Visibility: export

hall : HFunctor k l p => HFold k l p => (f a -> Bool) -> p f ks -> Bool

  Generalization of `all` to heterogeneous containers.

Totality: total
Visibility: export

hany : HFunctor k l p => HFold k l p => (f a -> Bool) -> p f ks -> Bool

  Generalization of `any` to heterogeneous containers.

Totality: total
Visibility: export

hchoice : HFold k l p => Alternative f => p (K (f a)) ks -> f a

  Generalization of `choice` to heterogeneous containers.

Totality: total
Visibility: export

interface HSequence : (k : Type) -> (l : Type) -> HCont k l -> Type

  Sequencing of applicative effects over a heterogeneous
  container.

Parameters: k, l, p
Methods:

hsequence : Applicative g => p (\a => g (f a)) ks -> g (p f ks)

  Given a heterogeneous containers holding values
  wrapped in effect `g`, sequences applications of
  `g` to the outside of the heterogeneous container.
  
  ```idris example
  seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
  seqMaybe = hsequence
  ```

Implementations:

HSequence k (List k) (NS_ k)

HSequence k (List k) (NP_ k)

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

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

hsequence : HSequence k l p => Applicative g => p (\a => g (f a)) ks -> g (p f ks)

  Given a heterogeneous containers holding values
  wrapped in effect `g`, sequences applications of
  `g` to the outside of the heterogeneous container.
  
  ```idris example
  seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
  seqMaybe = hsequence
  ```

Totality: total
Visibility: public export

htraverse : Applicative g => HFunctor k l p => HSequence k l p => (f a -> g (f' a)) -> p f ks -> g (p f' ks)

  Traverses a heterogeneous container by applying effectful
  function `fun`.
  
  ```idris example
  htraverseEx : NP (Either String) [Int,String] -> Maybe (NP I [Int,String])
  htraverseEx = htraverse (either (const Nothing) Just)
  ```

Totality: total
Visibility: export

hfor : Applicative g => HFunctor k l p => HSequence k l p => p f ks -> (f a -> g (f' a)) -> g (p f' ks)

  Flipped version of `htraverse`.

Totality: total
Visibility: export

hctraverse : Applicative g => HAp k l q p => HSequence k l p => (0 c : (k -> Type)) -> q c ks => (c a => f a -> g (f' a)) -> p f ks -> g (p f' ks)

  Constrained version of `htraverse`.
  
  ```idris example
  interface Read a where
    read : String -> Maybe a
  
  hctraverseEx : NP Read [Int,String] =>
                 NP (K String) [Int,String] -> Maybe (NP I [Int,String])
  hctraverseEx = hctraverse Read read
  ```

Totality: total
Visibility: export

hcfor : Applicative g => HAp k l q p => HSequence k l p => (0 c : (k -> Type)) -> q c ks => p f ks -> (c a => f a -> g (f' a)) -> g (p f' ks)

  Flipped version of `hctraverse`.

Totality: total
Visibility: export

interface HCollapse : (k : Type) -> (l : Type) -> HCont k l -> (Type -> Type) -> Type

  Collapsing a heterogeneous container to a homogeneous one
  of the same shape.

Parameters: k, l, p, collapseTo
Methods:

hcollapse : p (K a) ks -> collapseTo a

  A heterogeneous container over constant functor `K a` is
  actually a homogeneous one holding only values of type `a`.
  This function extracts the wrapped values into a homogeneous
  one of the same size and shape.

Implementations:

HCollapse k (List k) (NS_ k) I

HCollapse k (List k) (NP_ k) List

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

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

hcollapse : HCollapse k l p collapseTo => p (K a) ks -> collapseTo a

  A heterogeneous container over constant functor `K a` is
  actually a homogeneous one holding only values of type `a`.
  This function extracts the wrapped values into a homogeneous
  one of the same size and shape.

Totality: total
Visibility: public export