Idris2Doc : Nested

Nested

(source)
Definitions
NaturalTransformation : (k -> Type) -> (k -> Type) -> Type
  This serves as our higher-order "function" from `a` to `b`.

  Visibility: public export
Algebra : ((k -> Type) -> k -> Type) -> (k -> Type) -> Type
  Higher-order version of an "f-algebra" (i.e. `f a -> a`)

  Visibility: public export
Coalgebra : ((k -> Type) -> k -> Type) -> (k -> Type) -> Type
  Higher-order version of an "f-co-algebra" (i.e. `a -> f a`)

  Visibility: public export
HFunctor : ((k1 -> Type) -> k2 -> Type) -> Type
  Type of an higher-order mapping, a functor over type indexes.

  Visibility: public export
record Nested : (k -> Type) -> ((k -> Type) -> k -> Type) -> Type
  Serves as a proof that an indexed type (e.g.), `t`, is formed through nested
  (a.k.a. non-uniform) layers of the higher-order functor, `f`.

  Totality: total
  Visibility: public export
  Constructor: 
MkNested : HFunctor f -> Coalgebra f t -> Algebra f t -> Nested t f

  Projections:
  
.embed : Nested t f -> Algebra f t
  
.hfunctor : Nested t f -> HFunctor f
  
.project : Nested t f -> Coalgebra f t
.hfunctor : Nested t f -> HFunctor f
  Visibility: public export
hfunctor : Nested t f -> HFunctor f
  Visibility: public export
.project : Nested t f -> Coalgebra f t
  Visibility: public export
project : Nested t f -> Coalgebra f t
  Visibility: public export
.embed : Nested t f -> Algebra f t
  Visibility: public export
embed : Nested t f -> Algebra f t
  Visibility: public export
hfold : Nested t f -> Algebra f r -> NaturalTransformation t r
  Reduce a realized nested value bottom-up to a output with the same index.

  Visibility: export
hbuild : Nested t f -> (Algebra f x -> NaturalTransformation r x) -> NaturalTransformation r t
  Given an algebra-based transformation, prepare a transformation that acts
  as if it were unfolding a nested value, without reifying the nested
  structure.  Effectively substituting a call to the algebra for any
  constructors of `t`
  
  Universal property (for all n, a, and ghf):
    hfold n a . hbuild n ghf = ghf a

  Visibility: export
hunfold : Nested t f -> Coalgebra f r -> NaturalTransformation r t
  Build a nested value top-down to from a seed with the same index.

  Visibility: export
hdestroy : Nested t f -> (Coalgebra f x -> NaturalTransformation x r) -> NaturalTransformation t r
  Universal property (for all n, ghu, and c):
    hdestory n ghu . hunfold n c = ghu c

  Visibility: export
hhylo : HFunctor f -> Coalgebra f i -> Algebra f o -> NaturalTransformation i o
  Build a transformation with a nested recursion pattern, roughly equivalent
  to `hfold n a . hunfold n c`, but the nested type, `n`, is an implicit
  fixed-point of `f`.

  Visibility: export
Ran : (k -> Type) -> (k -> Type) -> Type -> Type
  Polykinded right Kan extension of `g` along `f`

  Visibility: public export
gfold : Nested t f -> Algebra f (Ran c r) -> (i -> c o) -> t i -> r o
  Index-changing fold via right Kan extension of the `r`esult functor along a
  `c`arrier functor.  A specialized version of `hfold` with some of the
  arguments rearranged.

  Visibility: export
record Lan : (k -> Type) -> (k -> Type) -> Type -> Type
  Polykinded left Kan extension of `g` along `f`

  Totality: total
  Visibility: public export
  Constructor: 
MkLan : (f target -> a) -> g target -> Lan f g a

  Projections:
  
.extract : ({rec:0} : Lan f g a) -> f (target {rec:0}) -> a
  
.pool : ({rec:0} : Lan f g a) -> g (target {rec:0})
  
.target : Lan f g a -> k
.target : Lan f g a -> k
  Visibility: public export
target : Lan f g a -> k
  Visibility: public export
.extract : ({rec:0} : Lan f g a) -> f (target {rec:0}) -> a
  Visibility: public export
extract : ({rec:0} : Lan f g a) -> f (target {rec:0}) -> a
  Visibility: public export
.pool : ({rec:0} : Lan f g a) -> g (target {rec:0})
  Visibility: public export
pool : ({rec:0} : Lan f g a) -> g (target {rec:0})
  Visibility: public export
gbuild : Nested t f -> (Algebra f x -> NaturalTransformation (Lan c s) x) -> (c i -> o) -> s i -> t o
  Like `gunfold`, but apply the algebra instead of the constructors of `t`.

  Visibility: export
gunfold : Nested t f -> Coalgebra f (Lan c s) -> (c i -> o) -> s i -> t o
  Index-changing unfold via left Kan extension of the `s`eed functor along
  a `c`arrier function.  A specialized version of `hunfold` with the "Lan"
  argument curried.

  Visibility: export
gdestroy : Nested t f -> (Coalgebra f x -> NaturalTransformation x (Ran c r)) -> (i -> c o) -> t i -> r o
  Like `hdestroy` in the same way that `gfold` is like `hfold`.
  
  Universal property:
    (gdestroy n ghu f . gunfold n c g) x = ghu c (MkLan g x) f

  Visibility: export
Codensity : (k -> Type) -> Type -> Type
  Codensity monad, the right Kan extension of a functor along itself

  Visibility: public export
ffold : Nested t f -> Algebra f (Codensity (Const a)) -> t a -> a
  Reduce to a single value of the index type.  A specialization of `gfold`.

  Visibility: export
Density : (k -> Type) -> Type -> Type
  Density comonad, the left Kan extension of a functor along itself.

  Visibility: public export
fbuild : Nested t f -> (Algebra f x -> NaturalTransformation (Density (Const a)) x) -> a -> t a
  Like `funfold` in the same way `gbuild` is like `gunfold`.  Specialization
  of `gbuild`.

  Visibility: export
funfold : Nested t f -> Coalgebra f (Density (Const a)) -> a -> t a
  Unfold from a single value, with the type of that value being the output
  index.  A specialization of `gunfold`.

  Visibility: export
fdestroy : Nested t f -> (Coalgebra f x -> NaturalTransformation x (Codensity (Const a))) -> t a -> a
  Like `ffold` in the same way `gdestroy` is like `gfold`.  Specialization of
  `gdestroy`.

  Visibility: export