Data.Container.Base.Morphism.Instances

Definitions

State : Cont -> Type

  "State" as defined in https://arxiv.org/abs/2403.13001 and open games 
  
        ┌─────────────┐
        │             ├──► (x : c.Shp)
        │    State    │
        │             ├◄── c.Pos x
        └─────────────┘

Totality: total
Visibility: public export

toState : c .Shp -> State c

  Given a shape of any container, state can be defined

Totality: total
Visibility: public export

fromState : State c -> c .Shp

Totality: total
Visibility: public export

mapState : State c -> c =%> d -> State d

Totality: total
Visibility: public export

Costate : Cont -> Type

  "Costate" as defined in https://arxiv.org/abs/2403.13001 and open games 
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             │
                   │   Costate   │
      c.Pos x   ◄──┤             │
                   └─────────────┘

Totality: total
Visibility: public export

toCostate : ((x : c .Shp) -> c .Pos x) -> Costate c

Totality: total
Visibility: public export

fromCostate : Costate c -> (x : c .Shp) -> c .Pos x

Totality: total
Visibility: public export

mapCostate : Costate d -> c =%> d -> Costate c

Totality: total
Visibility: public export

fromNapCostateToState : Costate (Nap (c .Shp)) -> State c

Totality: total
Visibility: public export

fromStateToNapCostate : State c -> Costate (Nap (c .Shp))

Totality: total
Visibility: public export

pushDown : Cont -> Cont

  If we model the idea of a container (S !> P) as a box
   ┌──────┐
   │ s:S  │
   ├──────┤
   │  Ps  │
   └──────┘
  then `pushDown` is interpreted as pushing down the container,
  pruning anything that goes out of the box, and using `Unit` for
  anything new that appears:
   ┌──────┐
   │ Unit │
   ├──────┤
   │ s:S  │
   └──────┘
      Ps

Totality: total
Visibility: public export

pushIntoContinuation : (d >< p) =%> l -> p =%> (pushDown d >@ l)

Totality: total
Visibility: public export

terminal : c =%> UnitCont

Totality: total
Visibility: public export

leftUnit : (Scalar >< c) =%> c

Totality: total
Visibility: public export

rightUnit : (c >< Scalar) =%> c

Totality: total
Visibility: public export

leftUnitInv : c =%> (Scalar >< c)

Totality: total
Visibility: public export

rightUnitInv : c =%> (c >< Scalar)

Totality: total
Visibility: public export

assocL : ((a >< b) >< c) =%> (a >< (b >< c))

Totality: total
Visibility: public export

assocR : (a >< (b >< c)) =%> ((a >< b) >< c)

Totality: total
Visibility: public export

swap : (a >< b) =%> (b >< a)

Totality: total
Visibility: public export

swapMiddle : ((c1 >< c2) >< (c3 >< c4)) =%> ((c1 >< c3) >< (c2 >< c4))

Totality: total
Visibility: public export

leftUnit : (Scalar >@ c) =%> c

Totality: total
Visibility: public export

rightUnit : (c >@ Scalar) =%> c

Totality: total
Visibility: public export

leftUnitInv : c =%> (Scalar >@ c)

Totality: total
Visibility: public export

rightUnitInv : c =%> (c >@ Scalar)

Totality: total
Visibility: public export

elim : (c >+< c) =%> c

Totality: total
Visibility: public export

initial : Empty =%> c

Totality: total
Visibility: public export

cojoin : c =%> z -> d =%> z -> (c >+< d) =%> z

Totality: total
Visibility: public export

direct : (a .Shp -> Bool) -> a =%> (a >+< a)

Totality: total
Visibility: public export

duoidal : ((c >@ d) >< (e >@ f)) =%> ((c >< e) >@ (d >< f))

  Interaction between composition and tensor product
  Swaps the operations, and middle two containers
  Not an isomorphism!

Totality: total
Visibility: public export

tensorToComp : (c >< f) =%> (c >@ f)

  Tensor product embeds into composition
  A special case of `duoidal`

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

distribute : (c >< e) =%> s -> (c >< (e >@ g)) =%> (s >@ g)

  Specific distributive law we need

Totality: total
Visibility: public export

wrapIntoVector : c =%> d -> Tensor [c] =%> Tensor [d]

  Wraps a dependent lens `c =%> d`
  into one of type `c >@ Scalar =%> d >@ Scalar`
  Needed because `c >@ Scalar` isn't automatically reduced to `c`

Totality: total
Visibility: public export

wrapIntoMatrix : (c >@ c') =%> (d >@ d') -> Tensor [c, c'] =%> Tensor [d, d']

Totality: total
Visibility: public export

wrapIntoVectorHancock : c =%> d -> HancockTensor [c] =%> HancockTensor [d]

  Wraps a dependent lens `c =%> d`
  into one of type `c >< Scalar =%> d >< Scalar`
  Needed because `c >< Scalar` isn't automatically reduced to `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

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

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

inorderBackward : (b : BinTreeShape) -> Fin (numNodesAndLeaves b) -> BinTreePos b

Totality: total
Visibility: public export

inorder : BinTree =%> List

Totality: total
Visibility: public export

inorderBackward : (b : BinTreeShape) -> Fin (numNodes b) -> BinTreePosNode b

Totality: total
Visibility: public export

inorder : BinTreeNode =%> List

  Traverses a binary tree container in order, producing a list container

Totality: total
Visibility: public export

preorderBinTreeNode : (b : BinTreeShape) -> Fin (numNodes b) -> BinTreePosNode b

Totality: total
Visibility: public export

inorderBackward : (b : BinTreeShape) -> Fin (numLeaves b) -> BinTreePosLeaf b

Totality: total
Visibility: public export

inorder : BinTreeLeaf =%> List

Totality: total
Visibility: public export

vectToList : Vect n =%> List

Totality: total
Visibility: public export

maybeToList : Maybe =%> List

Totality: total
Visibility: public export

Sample : MonadSample m => IsSucc n => (m <!> Sample n) =%> Scalar

Totality: total
Visibility: public export

handleEffect : Monad m => (m <!> effect) =%> Scalar -> a =%> effect -> (m <!> a) =%> Scalar

Totality: total
Visibility: public export