Data.Container.Base.Properties.Instances

Definitions

EmptyExt : IsNaperian c => Ext c ()

Totality: total
Visibility: public export

liftA2ConstCont : IsNaperian c => Ext c a -> Ext c b -> Ext c (a, b)

Totality: total
Visibility: public export

compToTensor : IsNaperian d => (c >@ d) =%> (c >< d)

  Going the other way is impossible without any constraints
  Two possibilities on constraints (this, and `compToTensor2`)

Totality: total
Visibility: public export

compToTensor2 : IsFlat c => (c >@ d) =%> (c >< d)

Totality: total
Visibility: public export

transposeLens : IsNaperian c => IsNaperian d => (c >@ d) =%> (d >@ c)

Totality: total
Visibility: public export

transpose : IsNaperian c => IsNaperian d => Tensor [c, d] =%> Tensor [d, c]

Totality: total
Visibility: public export

cubicalShapeHelper : All IsCubical shape -> List Nat

  Helper function allowing `shape` in `cubicalShape` to have zero annotation

Totality: total
Visibility: public export

cubicalShape : (0 shape : List Cont) -> All IsCubical shape => List Nat

  Given a list of cubical containers, return the list of their dimensions

Totality: total
Visibility: public export

size : (0 shape : List Cont) -> All IsCubical shape => Nat

  Size of a list of cubical containers is the product of their dimensions

Totality: total
Visibility: public export

flattenCubical : {auto ac : All IsCubical shape} -> LayoutOrder -> Tensor shape =%> Vect (size shape)

  Layout-aware dependent lens flattening a cubical tensor

Totality: total
Visibility: public export

unflattenCubical : {auto ac : All IsCubical shape} -> LayoutOrder -> Vect (size shape) =%> Tensor shape

  Layout-aware dependent lens unflattening a tensor

Totality: total
Visibility: public export

recastFlattenedTensor : {auto oldAc : All IsCubical oldShape} -> {auto newAc : All IsCubical newShape} -> size oldShape = size newShape => Vect (size oldShape) =%> Vect (size newShape)

  This is simply a rewrite!

Totality: total
Visibility: public export

reshape : {auto oldAc : All IsCubical oldShape} -> {auto newAc : All IsCubical newShape} -> LayoutOrder -> size oldShape = size newShape => Tensor oldShape =%> Tensor newShape

  Reshapes a cubical tensor by first flattening it to a linear representation,
  casting the type to the new shape, and then unflattening it back
  Is generic over layout order

Totality: total
Visibility: public export

hancockTensorNaperianShape : All IsNaperian shape => (HancockTensor shape) .Shp

Totality: total
Visibility: public export

tensorNaperianShape : All IsNaperian shape => (Tensor shape) .Shp

  Helper to compute the unique shape of Tensor when all containers are Naperian

Totality: total
Visibility: public export

hancockTensorPosEq : All IsNaperian shape => (HancockTensor shape) .Pos x = (HancockTensor shape) .Pos y

  Analogous to `naperianPosEq` but for the HancockTensor structure
  We can't use `naperianPosEq` directly because the shape of the resulting
  container is not Unit, it is only isomorphic to it

Totality: total
Visibility: public export

transformToHancock : All IsNaperian shape => Tensor shape =%> HancockTensor shape

  Tensor shape is isomorphic to HancockTensor shape when all containers in
  the shape are Naperian. This is one arrow of that isomorphism

Totality: total
Visibility: public export

transformFromHancock : All IsNaperian shape => HancockTensor shape =%> Tensor shape

Totality: total
Visibility: public export

lambdaNap : IsConcrete (Nap s)

  This is a concrete instance for Naperian containers
  It applies also to `s=Fin n` which is covered by Vect
  We therefore want this to only be applied if Vect isn't

Totality: total
Visibility: public export

maybeIsDecidable : IsDecidable Maybe

Totality: total
Visibility: public export

maybeTwoIsDecidable : IsDecidable MaybeTwo

Totality: total
Visibility: public export

compositionIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >@ d)

Totality: total
Visibility: public export

hancockIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >< d)

  Positions are pairs of positions

Totality: total
Visibility: public export

cartesianIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >*< d)

  Positions are a position of one or of the other

Totality: total
Visibility: public export

coproductIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >+< d)

  Positions are those of whichever container the shape comes from

Totality: total
Visibility: public export

tensorIsDecidable : All IsDecidable cs => IsDecidable (Tensor cs)

  `cs` can't be inferred from `Tensor cs`, so pass it as `{cs = ...}`.
  The `All` itself is found by search when the containers in `cs` are

Totality: total
Visibility: public export

enumerableIsFoldable : IsEnumerable c => IsFoldable c

  Every enumeration is a fold, forgetting the map from positions to indices

Totality: total
Visibility: public export

listIsEnumerable : IsEnumerable List

  Lists, non-empty lists and vectors number their own positions

Totality: total
Visibility: public export

list1IsEnumerable : IsEnumerable List1

Totality: total
Visibility: public export

vectIsEnumerable : IsEnumerable (Vect n)

Totality: total
Visibility: public export

forgetOrder : List =%> Bag

  Forgetting the order of a list gives a bag

Totality: total
Visibility: public export

foldableIsSummable : IsFoldable c => IsSummable c

  Every foldable container is summable, through the order its fold chose

Totality: total
Visibility: public export

foldableAt : IsFoldable c => (s : c .Shp) -> IsFoldable (At c s)

  A foldable container restricted to one of its shapes is foldable

Totality: total
Visibility: public export

index : IsFoldable c => Pick c a =%> List

  Every extension of a foldable container indexes as a list

Totality: total
Visibility: public export

binTreeLeafIsEnumerable : IsEnumerable BinTreeLeaf

  Requires making a choice of traversal order
  Is there a good reason to prefer a particular order?
  The index of a position and the two round trips are not written yet

Totality: total
Visibility: public export

binTreeNodeIsEnumerable : IsEnumerable BinTreeNode

Totality: total
Visibility: public export

binTreeIsEnumerable : IsEnumerable BinTree

Totality: total
Visibility: public export

algebraFoldable : Foldable f => Num a => Algebra f a

  Any foldable functor can be given an algebra by summing its values

Totality: total
Visibility: public export

argmax : Ord a => IsFoldable c => IsNonEmpty c => (e : Ext c a) -> c .Pos (shapeExt e)

Totality: total
Visibility: public export