Data.Container.Base.Morphism.Instances

Definitions

State : Cont -> Type

  "State" as defined in https://arxiv.org/abs/2403.13001 and open games 
  Given a shape of any container, state can be defined

Visibility: public export

Costate : Cont -> Type

Visibility: public export

toState : c .Shp -> State c

Visibility: public export

fromState : State c -> c .Shp

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

pushDown : Cont -> Cont

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

  Interaction between composition and tensor product

Visibility: public export

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

  Specific distributive law we need

Visibility: public export

extMap : c =%> d -> Ext c a -> Ext d a

  Ext is a functor of type Cont -> [Type, Type]
  On objects it maps a container to a polynomial functor
  On morphisms it maps a dependent lens to a natural transformation
  This is the action on morphisms

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`

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`

Visibility: public export

cubicalShapeHelper : All IsCubical shape -> List Nat

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

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

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

Visibility: public export

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

  Layout-aware dependent lens flattening a cubical tensor

Visibility: public export

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

  Layout-aware dependent lens unflattening a tensor

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!

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

Visibility: public export

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

Visibility: public export

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

  This and the above function should be one and the same, up to rebracketing

Visibility: public export

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

Visibility: public export

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

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

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

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

Visibility: public export

EmptyExtEq : IsNaperian c => Ext c () = ()

Visibility: public export

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

Visibility: public export

inorder : BinTree =%> List

Visibility: public export

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

Visibility: public export

inorder : BinTreeNode =%> List

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

Visibility: public export

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

Visibility: public export

maybeToList : Maybe =%> List

Visibility: public export

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

Visibility: public export

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

Visibility: public export