Idris2Doc : Data.Container.Base.Properties.Definition

Data.Container.Base.Properties.Definition

(source)
Reexports
import public Decidable.Equality
Definitions
interface MapToWith : (Type -> Type) -> Cont -> Cont -> Type
  The data of a lens from `d`, with `i` on its positions into `c`. Used to 
  generically define `IsFoldable`, `IsSummable`, and `InterfaceOnPositions`

  Parameters: i, c, d
Constructor: 
Along

Methods:
  
mapTo : (i <!> d) =%> c

Implementations:
  
((s : c .Shp) -> i (c .Pos s)) => InterfaceOnPositions c i
  
IsDecidable Maybe
  
IsDecidable MaybeTwo
  
IsEnumerable c => IsFoldable c
  
IsFoldable c => IsSummable c
mapTo : MapToWith i c d => (i <!> d) =%> c
  Totality: total
  Visibility: public export
MapTo : {default id _ : (Type -> Type)} -> Cont -> Cont -> Type
  Totality: total
  Visibility: public export
InterfaceOnPositions : Cont -> (Type -> Type) -> Type
  Stores the data of a container `c` with an interface `i` on its positions
  As a lens `i <!> c =%> Scalar` it is a costate of `i <!> c`

  Totality: total
  Visibility: public export
MkI : ((s : c .Shp) -> i (c .Pos s)) -> InterfaceOnPositions c i
  Totality: total
  Visibility: public export
GetInterface : InterfaceOnPositions c i -> (s : c .Shp) -> i (c .Pos s)
  For every shape `s` the set of positions `c.Pos s` has that interface

  Totality: total
  Visibility: public export
fromPositions : ((s : c .Shp) -> i (c .Pos s)) => InterfaceOnPositions c i
  Totality: total
  Visibility: public export
IsDecidable : Cont -> Type
  A container is decidable if for every shape its set of positions has 
  decidable equality

  Totality: total
  Visibility: public export
IsNonEmpty : Cont -> Type
  A container is non-empty when for every shape the set of positions is
  non-empty. It's witnessed constructively by choosing a position for every
  shape. It's also the same data as a costate of a container.
  TODO can this be done without a specific witness?

  Totality: total
  Visibility: public export
ChosenPositions : Cont -> Type
  Name more accurately reflecting the fact that position choice is arbitrary

  Totality: total
  Visibility: public export
data IsA : Cont -> (0 _ : (a -> Cont)) -> Type
  Proof that a container `c` of the form `f x` for some `x`.
  Does not work with two arguments, i.e. this 
  (https://github.com/bgavran/TensorType/blob/cc67c8b4461467874a55af7756e1b4a7f768c1f0/src/Data/Container/Base/Properties/Definition.idr#L63) does not work with this definition, and would instead 
  require a `IsA2`. (That particular example was removed because nothing 
  depended on it)

  Totality: total
  Visibility: public export
  Constructor: 
Via : (x : a) -> IsA (f x) f
IsFlat : Cont -> Type
  Totality: total
  Visibility: public export
IsSharp : Cont -> Type
  Totality: total
  Visibility: public export
IsConst : Cont -> Type
  Used in learning, where we want to know that the tangent space over a
  particular parameter is equal to the parameter space itself

  Totality: total
  Visibility: public export
IsNaperian : Cont -> Type
  Notably, Naperian does not imply Finite (`Stream` is Naperian)

  Totality: total
  Visibility: public export
LogHelper : IsNaperian c => Type
  Totality: total
  Visibility: public export
Log : (0 c : Cont) -> IsNaperian c => Type
  Totality: total
  Visibility: public export
naperianPosEq : IsNaperian c => c .Pos x = c .Pos y
  Totality: total
  Visibility: public export
IsCubical : Cont -> Type
  A container is cubical whenever it is Finite and Naperian.
  All of such containers are `Vect n`, up to isomorphism. Notably, this also 
  includes a container whose positions are the set of positions of a binary 
  tree of a particular shape.  This is isomorphic to the `Vect k` container, 
  for some `k`, assuming a choice of tree traversal

  Totality: total
  Visibility: public export
dimHelper : IsCubical c -> Nat
  Totality: total
  Visibility: public export
dim : (0 c : Cont) -> IsCubical c => Nat
  We call dimension the size of the set of positions of a finite container 

  Totality: total
  Visibility: public export
isCubicalContEq : ({arg:12902} : IsCubical d) -> d = Vect (dim d)
  Every cubical container is `Vect n` with `n = dim ic` (used for rewrites).

  Totality: total
  Visibility: public export
IsFoldable : Cont -> Type
  A container is foldable if there exists a lens `c =%> List`
  Notably, this isn't required to be an isomorphism. For instance, binary 
  trees (with ordered branches) are foldable, but not isomorphic to lists.

  Totality: total
  Visibility: public export
IsSummable : Cont -> Type
  A container is summable if there is a dependent lens `c =%> Bag`. That is,
  a fold whose order does not matter.

  Totality: total
  Visibility: public export
mapToList : IsFoldable c => c =%> List
  The lens of a foldable container into `List`
  Ideally we would not need this, but `id <!> c` does not reduce to `c`

  Totality: total
  Visibility: public export
mapToBag : IsSummable c => c =%> Bag
  Totality: total
  Visibility: public export
interface IsEnumerable : Cont -> Type
  A container is enumerable when at every shape its positions are in
  bijection with `Fin n`, i.e. there is a cartesian morphism into `List`
  Are these lawful traversables? Every position is visited exactly once, in a 
  chosen order.  Unlike with `IsFoldable`, positions can neither be skipped 
  nor repeated

  Parameters: c
Constructor: 
MkIsEnum

Methods:
  
enumerate : c =:> List

Implementations:
  
IsEnumerable List
  
IsEnumerable List1
  
IsEnumerable (Vect n)
  
IsEnumerable BinTreeLeaf
  
IsEnumerable BinTreeNode
  
IsEnumerable BinTree
enumerate : IsEnumerable c => c =:> List
  Totality: total
  Visibility: public export
interface IsConcrete : Cont -> Type
  Many datatypes in the Idris standard library are already
  concrete representations of particular containers

  Parameters: c
Constructor: 
MkIsConcrete

Methods:
  
func : Type -> Type
  
functorInstance : Functor func
  
fromConcreteTy : func a -> Ext c a
  
toConcreteTy : Ext c a -> func a

Implementations:
  
IsConcrete RoseTree
  
IsConcrete Scalar
  
IsConcrete UnitCont
  
IsConcrete Maybe
  
IsConcrete Pair
  
IsConcrete c => IsConcrete d => IsConcrete (c >< d)
  
IsConcrete c => IsConcrete d => IsConcrete (c >@ d)
  
IsConcrete List
  
IsConcrete (Vect n)
  
IsConcrete (Grid (h, w))
  
IsConcrete BinTree
  
IsConcrete BinTreeNode
  
IsConcrete BinTreeLeaf
func : IsConcrete c => Type -> Type
  Totality: total
  Visibility: public export
functorInstance : {auto __con : IsConcrete c} -> Functor func
  Totality: total
  Visibility: public export
fromConcreteTy : {auto __con : IsConcrete c} -> func a -> Ext c a
  Totality: total
  Visibility: public export
toConcreteTy : {auto __con : IsConcrete c} -> Ext c a -> func a
  Totality: total
  Visibility: public export
(>#) : {auto {conArg:13126} : IsConcrete c} -> func a -> Ext c a
  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 0
(#>) : {auto {conArg:13148} : IsConcrete c} -> Ext c a -> func a
  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 0