Idris2Doc : Data.SOP.NS

Data.SOP.NS

(source)
Definitions
data NS_ : (k : Type) -> (k -> Type) -> List k -> Type
  An n-ary sum.
  
  The sum is parameterized by a type constructor f and indexed by a
  type-level list xs. The length of the list determines the number of choices
  in the sum and if the i-th element of the list is of type x, then the i-th
  choice of the sum is of type f x.
  
  The constructor names are chosen to resemble Peano-style natural numbers,
  i.e., Z is for "zero", and S is for "successor". Chaining S and Z chooses
  the corresponding component of the sum.
  
  Note that empty sums (indexed by an empty list) have no non-bottom
  elements.
  
  Two common instantiations of f are the identity functor I and the constant
  functor K. For I, the sum becomes a direct generalization of the Either
  type to arbitrarily many choices. For K a, the result is a homogeneous
  choice type, where the contents of the type-level list are ignored, but its
  length specifies the number of options.
  
  In the context of the SOP approach to generic programming, an n-ary sum
  describes the top-level structure of a datatype, which is a choice between
  all of its constructors.
  
  Examples:
  
  ```idris example
  the (NS_ Type I [Char,Bool]) (Z 'x')
  the (NS_ Type I [Char,Bool]) (S $ Z False)
  ```

  Totality: total
  Visibility: public export
  Constructors:
  
Z : f t -> NS_ k f (t :: ks)
  
S : NS_ k f ks -> NS_ k f (t :: ks)

  Hints:
  
NP (DecEq . f) ks => DecEq (NS_ k f ks)
  
NP (Eq . f) ks => Eq (NS_ k f ks)
  
HAp k (List k) (NP_ k) (NS_ k)
  
HCollapse k (List k) (NS_ k) I
  
HFold k (List k) (NS_ k)
  
HFunctor k (List k) (NS_ k)
  
HSequence k (List k) (NS_ k)
  
NP (Monoid . f) [k'] => Monoid (NS_ k f [k'])
  
NP (Ord . f) ks => Ord (NS_ k f ks)
  
NP (Semigroup . f) [k'] => Semigroup (NS_ k f [k'])
  
NP (Show . f) ks => Show (NS_ k f ks)
  
Uninhabited (Z x = S y)
  
Uninhabited (S x = Z y)
NS : (k -> Type) -> List k -> Type
  Type alias for `NS_` with type parameter `k` being
  implicit. This reflects the kind-polymorphic data type
  in Haskell.

  Totality: total
  Visibility: public export
toI : NS_ k f ks -> NS I (map f ks)
  Changes an n-ary sum to the identity context `I`
  by adjusting the types of stored values accordingly.

  Totality: total
  Visibility: public export
mapNS : (f a -> g a) -> NS f ks -> NS g ks
  Specialiced version of `hmap`

  Totality: total
  Visibility: public export
foldlNS : (acc -> el -> acc) -> acc -> NS (K el) ks -> acc
  Specialization of `hfoldl`

  Totality: total
  Visibility: public export
foldrNS : (el -> Lazy acc -> acc) -> Lazy acc -> NS (K el) ks -> acc
  Specialization of `hfoldr`

  Totality: total
  Visibility: public export
sequenceNS : Applicative g => NS (\a => g (f a)) ks -> g (NS f ks)
  Specialization of `hsequence`

  Totality: total
  Visibility: public export
hapNS : NP (\a => f a -> g a) ks -> NS f ks -> NS g ks
  Specialization of `hap`

  Totality: total
  Visibility: public export
collapseNS : NS (K a) ks -> a
  Specialization of `hcollapse`

  Totality: total
  Visibility: public export
0 Injection : (k -> Type) -> List k -> k -> Type
  An injection into an n-ary sum takes a value of the correct
  type and wraps it in one of the sum's possible choices.

  Totality: total
  Visibility: public export
injectionsNP : NP g ks -> NP (Injection f ks) ks
  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
injections : NP (Injection f ks) ks
  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
apInjsNP_ : NP f ks -> NP (K (NS f ks)) ks
  Applies all injections to an n-ary product of values.
  
  This is not implemented in terms of injections for the
  following reason: Since we have access to the structure
  of the n-ary product and thus `ks`, we do not need a
  runtime reference of `ks`. Therefore, when applying
  injections to an n-ary product, prefer this function
  over a combination involving `injections`.

  Totality: total
  Visibility: public export
apInjsNP : NP f ks -> List (NS f ks)
  Alias for `collapseNP . apInjsNP_`

  Totality: total
  Visibility: public export
inject : f t -> Elem t ks => NS f ks
  Injects a value into an n-ary sum.

  Totality: total
  Visibility: public export
extract : (0 t : k) -> NS f ks -> Elem t ks => Maybe (f t)
  Tries to extract a value of the given type from an n-ary sum.

  Totality: total
  Visibility: public export
toNP : Alternative g => NS f ks -> NP (g . f) ks
  Converts an n-ary sum into the corresponding n-ary product
  of alternatives.

  Totality: total
  Visibility: public export
expand : NS f ks -> Sublist ks ks' => NS f ks'
  Injects an n-ary sum into a larger n-ary sum.

  Totality: total
  Visibility: public export
narrow : NS f ks -> Sublist ks' ks => Maybe (NS f ks')
  Tries to narrow down an n-ary sum to a subset of
  choices. `ks'` must be a sublist (values in the same order) of `ks`.

  Totality: total
  Visibility: public export