Idris2Doc : Data.SOP.NP

Data.SOP.NP

(source)
Definitions
data NP_ : (k : Type) -> (k -> Type) -> List k -> Type
  An n-ary product.
  
  The product is parameterized by a type constructor f and indexed by a
  type-level list ks. The length of the list determines the number of
  elements in the product, and if the i-th element of the list is of type k,
  then the i-th element of the product is of type f k.
  
  Two common instantiations of f are the identity functor I and the constant
  functor K. For I, the product becomes a heterogeneous list, where the
  type-level list describes the types of its components.  For K a, the product
  becomes a homogeneous list, where the contents of the type-level list are
  ignored, but its length still specifies the number of elements.
  
  In the context of the SOP approach to generic programming, an n-ary product
  describes the structure of the arguments of a single data constructor.
  
  Note: `NP_` takes an additional type parameter `k` to simulate
        Haskell's kind polymorphism. In theory, this could be left
        as an implicit argument. However, type-inference when calling
        interface functions like `hpure` was rather poor with `k`
        being implicit.
  
        We therefore made `k` explicit and added a type alias `NP`
        to be used in those occasions when `k` can be inferred.
  
  Examples:
  
  ```idris example
  ex1 : NP I [Char,Bool]
  ex1 = ['c',False]
  
  ex2 : NP (K String) [Char,Bool,Int]
  ex2 = ["Hello","World","!"]
  
  ex3 : NP Maybe [Char,Bool,Int]
  ex3 = [Just 'x', Nothing, Just 1]
  ```

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : NP_ k f []
  
(::) : f t -> NP_ k f ks -> NP_ k f (t :: ks)

  Hints:
  
NP (DecEq . f) ks => DecEq (NP_ k f ks)
  
NP (Eq . f) ks => Eq (NP_ k f ks)
  
HAp k (List k) (NP_ k) (NS_ k)
  
HAp k (List k) (NP_ k) (NP_ k)
  
HCollapse k (List k) (NP_ k) List
  
HFold k (List k) (NP_ k)
  
HFunctor k (List k) (NP_ k)
  
HPure k (List k) (NP_ k)
  
HSequence k (List k) (NP_ k)
  
NP (Monoid . f) ks => Monoid (NP_ k f ks)
  
POP_ k (c . f) kss -> (NP_ k (c . f) ks => c (NP_ k f ks)) => NP_ (List k) (c . NP_ k f) kss
  
NP (Ord . f) ks => Ord (NP_ k f ks)
  
NP (Semigroup . f) ks => Semigroup (NP_ k f ks)
  
NP (Show . f) ks => Show (NP_ k f ks)
NP : (k -> Type) -> List k -> Type
  Type alias for `NP_` with type parameter `k` being
  implicit. This reflects the kind-polymorphic data type
  in Haskell.

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

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

  Totality: total
  Visibility: public export
pureNP : f a -> NP f ks
  Specialization of `hpure`.

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

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

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

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

  Totality: total
  Visibility: public export
collapseNP : NP (K a) ks -> List a
  Specialization of `hcollapse`

  Totality: total
  Visibility: public export
hd : NP f (k :: ks) -> f k
  Returns the head of a non-empty n-ary product

  Totality: total
  Visibility: public export
tl : NP f (k :: ks) -> NP f ks
  Returns the tail of a non-empty n-ary product

  Totality: total
  Visibility: public export
fromListNP : NP f ks -> List a -> Maybe (NP (K a) ks)
  Tries to creates a homogeneous n-ary product of the given
  shape from a list of values.

  Totality: total
  Visibility: public export
fromList : List a -> Maybe (NP (K a) ks)
  Like `fromListNP` but takes the shape from the implicit
  list of types.

  Totality: total
  Visibility: public export
unfoldNP : NP f ks -> (s -> (s, a)) -> s -> NP (K a) ks
  Creates a homogeneous n-ary product of the given
  shape by repeatedly applying a function to a seed value.

  Totality: total
  Visibility: public export
unfold : (s -> (s, a)) -> s -> NP (K a) ks
  Like `unfoldNP` but takes the shape from the implicit
  list of types.

  Totality: total
  Visibility: public export
iterateNP : NP f ks -> (a -> a) -> a -> NP (K a) ks
  Creates a homogeneous n-ary product of the given
  shape using an initial value and a function for
  generating the next value.

  Totality: total
  Visibility: public export
iterate : (a -> a) -> a -> NP (K a) ks
  Like `iterate` but takes the shape from the implicit
  list of types.

  Totality: total
  Visibility: public export
0 Projection : (k -> Type) -> List k -> k -> Type
  A projection of an n-ary product p extracts the
  value of p at a certain position.

  Totality: total
  Visibility: public export
projections : NP (Projection f ks) ks
  The set of projections of an n-ary product `NP f ks` can
  itself be wrapped in an n-ary product of the same shape.

  Totality: total
  Visibility: public export
get : (0 t : k) -> Elem t ks => NP_ k f ks -> f t
  Access the first element of the given type in
  an n-ary product

  Totality: total
  Visibility: public export
modify : (f t -> f t') -> UpdateOnce t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Modify a single element of the given type
  in an n-ary product, thereby possibly changing the
  types of stored values.

  Totality: total
  Visibility: public export
modifyF : Functor g => (f t -> g (f t')) -> UpdateOnce t t' ks ks' => NP_ k f ks -> g (NP_ k f ks')
  Modify a single element of the given type
  in an n-ary product by applying an effectful
  function.
  
  This is the effectful version of `modify`.

  Totality: total
  Visibility: public export
modifyMany : (f t -> f t') -> UpdateMany t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Modify several elements of the given type
  in an n-ary product, thereby possibly changing the
  types of stored values.

  Totality: total
  Visibility: public export
modifyManyF : Applicative g => (f t -> g (f t')) -> UpdateMany t t' ks ks' => NP_ k f ks -> g (NP_ k f ks')
  Modify several elements of the given type
  in an n-ary product by applying an effectful function.
  
  This is the effectful version of `modifyMany`.

  Totality: total
  Visibility: public export
setAt : (0 t : k) -> f t' -> UpdateOnce t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Replaces the first element of the given type
  in an n-ary product, thereby possibly changing the
  types of stored values.

  Totality: total
  Visibility: public export
setAtMany : (0 t : k) -> f t' -> UpdateMany t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Replaces several elements of the given type
  in an n-ary product, thereby possibly changing the
  types of stored values.

  Totality: total
  Visibility: public export
setAt' : (0 t : k) -> (0 t' : k) -> f t' -> UpdateOnce t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Alias for `setAt` for those occasions when
  Idris cannot infer the type of the new value.

  Totality: total
  Visibility: public export
setAtMany' : (0 t : k) -> (0 t' : k) -> f t' -> UpdateMany t t' ks ks' => NP_ k f ks -> NP_ k f ks'
  Alias for `setAtMany` for those occasions when
  Idris cannot infer the type of the new value.

  Totality: total
  Visibility: public export
narrow : NP f ks -> Sublist ks' ks => NP f ks'
  Extracts a subset of values from an n-ary product.
  The values must appear in the same order in both lists.

  Totality: total
  Visibility: public export
append : NP f ks -> NP f ks' -> NP f (ks ++ ks')
  Appends two n-ary products.

  Totality: total
  Visibility: public export
expand : f k -> NP f ks -> Sublist ks ks' => NP f ks'
  Expands an n-ary product by filling missing
  values with the given default-generating function.

  Totality: total
  Visibility: public export
cexpand : (0 c : (k -> Type)) -> NP c ks' => (c k => f k) -> Sublist ks ks' => NP_ k f ks -> NP_ k f ks'
  Expands an n-ary product by filling missing
  values with the given default-generating function.
  
  This is the constrained version of `expand`.

  Totality: total
  Visibility: public export
ordToEqNP : NP (Ord . f) ks -> NP (Eq . f) ks
  This is needed to implement `Ord` below.

  Totality: total
  Visibility: public export
monoidToSemigroupNP : NP (Monoid . f) ks -> NP (Semigroup . f) ks
  This is needed to implement `Monoid` below.

  Totality: total
  Visibility: public export