
   0 | module Data.Container.Base.Morphism.Instances
   1 | 
   2 | import Data.Fin
   3 | import Data.Fin.Split
   4 | import Data.Vect
   5 | import Data.List.Elem
   6 | import Data.List.Quantifiers
   7 | 
   8 | import Data.Container.Base.Object.Definition
   9 | import Data.Container.Base.Morphism.Definition
  10 | import Data.Container.Base.Extension.Definition
  11 | import Data.Container.Base.Product.Definition
  12 | import Data.Container.Base.Endofunctor.Definition
  13 | 
  14 | import Data.Container.Base.Object.Instances
  15 | import Data.Container.Base.Extension.Instances
  16 | 
  17 | import Data.Container.Base.Quantifiers
  18 | import Data.Container.Base.TreeUtils
  19 | 
  20 | 
  21 | import Data.Num
  22 | import Data.Layout
  23 | import Misc
  24 | 
  25 | ||| If we model the idea of a container (S !> P) as a box
  26 | |||  ┌──────┐
  27 | |||  │ s:S  │
  28 | |||  ├──────┤
  29 | |||  │  Ps  │
  30 | |||  └──────┘
  31 | ||| then `pushDown` is interpreted as keeping the box frame in place while
  32 | ||| pushing down the container: pruning any part of the container that goes 
  33 | ||| out of the box, and using `Unit` for anything new that appears:
  34 | |||  ┌──────┐
  35 | |||  │ Unit │
  36 | |||  ├──────┤
  37 | |||  │ s:S  │
  38 | |||  └──────┘
  39 | |||     Ps
  40 | public export
  41 | pushDown : Cont -> Cont
  42 | pushDown c = Const2 Unit c.Shp
  43 | 
  44 | public export
  45 | pushIntoContinuation : {0 d, p, l : Cont} ->
  46 |   d >< p =%> l ->
  47 |   p =%> (pushDown d) >@ l
  48 | pushIntoContinuation f = !% \p => (() <| \d => f.fwd (d, p) **
  49 |   \(d ** l') => snd $ f.bwd (d, p) l')
  50 | 
  51 | 
  52 | namespace CategoricalProduct
  53 |   public export
  54 |   terminal : c =%> UnitCont
  55 |   terminal = !% \_ => (() ** absurd)
  56 | 
  57 | 
  58 | namespace HancockTensorProduct
  59 |   public export
  60 |   leftUnit : Scalar >< c =%> c
  61 |   leftUnit = !% \((), s) => (s ** \p => ((), p))
  62 |   
  63 |   public export
  64 |   rightUnit : c >< Scalar =%> c
  65 |   rightUnit = !% \(x, ()) => (x ** \x' => (x', ()))
  66 | 
  67 |   public export
  68 |   leftUnitInv : c =%> Scalar >< c
  69 |   leftUnitInv = !% \x => (((), x) ** \((), x') => x')
  70 | 
  71 |   public export
  72 |   rightUnitInv : c =%> c >< Scalar
  73 |   rightUnitInv = !% \x => ((x, ()) ** \(x', ()) => x')
  74 | 
  75 |   public export
  76 |   assocL : (a >< b) >< c =%> a >< (b >< c)
  77 |   assocL = !% \((a, b), c) => ((a, (b, c)) ** \(a', (b', c')) => ((a', b'), c'))
  78 | 
  79 |   public export
  80 |   assocR : a >< (b >< c) =%> (a >< b) >< c
  81 |   assocR = !% \(a, (b, c)) => (((a, b), c) ** \((a', b'), c') => (a', (b', c')))
  82 | 
  83 |   public export
  84 |   swap : a >< b =%> b >< a
  85 |   swap = !% \(a, b) => ((b, a) ** \(b', a') => (a', b'))
  86 | 
  87 |   public export
  88 |   swapMiddle : (c1 >< c2) >< (c3 >< c4) =%> (c1 >< c3) >< (c2 >< c4)
  89 |   swapMiddle = assocL {c=_ >< _}
  90 |            %>> (id >< assocR)
  91 |            %>> (id >< swap >< id)
  92 |            %>> (id >< assocL)
  93 |            %>> assocR {c=_ >< _}
  94 | 
  95 | namespace CompositionProduct
  96 |   public export
  97 |   leftUnit : Scalar >@ c =%> c
  98 |   leftUnit = !% \ex => (index ex () ** \c' => (() ** c'))
  99 | 
 100 |   public export
 101 |   rightUnit : c >@ Scalar =%> c
 102 |   rightUnit = !% \ex => (shapeExt ex ** \cp => (cp ** ()))
 103 | 
 104 |   public export
 105 |   leftUnitInv : c =%> Scalar >@ c
 106 |   leftUnitInv = !% \s => (() <| (\_ => s) ** \(() ** c') => c')
 107 |   
 108 |   public export
 109 |   rightUnitInv : c =%> c >@ Scalar
 110 |   rightUnitInv = !% \s => (s <| \_ => () ** fst)
 111 | 
 112 |   public export
 113 |   assocL : (a >@ b) >@ c =%> a >@ (b >@ c)
 114 |   assocL = !% \((aShp <| f) <| g) =>
 115 |     (aShp <| \aPos => f aPos <| \bPos => g (aPos  ** bPos) **
 116 |       \(aPos ** bPos ** cPos) => ((aPos ** bPos) ** cPos))
 117 | 
 118 |   public export
 119 |   assocR : a >@ (b >@ c) =%> (a >@ b) >@ c
 120 |   assocR = !% \(aShp <| f) =>
 121 |     ((aShp <| shapeExt . f) <| \(aPos ** bPos) => index (f aPos) bPos **
 122 |       \((aPos ** bPos) ** cPos) => (aPos ** (bPos ** cPos)))
 123 | 
 124 | namespace Coproduct
 125 |   public export
 126 |   elim : c >+< c =%> c
 127 |   elim = !% \case
 128 |     Left x => (x ** id)
 129 |     Right y => (y ** id)
 130 | 
 131 |   public export
 132 |   initial : Empty =%> c
 133 |   initial = !% absurd
 134 | 
 135 |   public export
 136 |   cojoin : c =%> z ->
 137 |     d =%> z ->
 138 |     c >+< d =%> z
 139 |   cojoin f g = (f >+< g) %>> elim
 140 | 
 141 |   public export
 142 |   direct : (a.Shp -> Bool) ->
 143 |     a =%> a >+< a
 144 |   direct p = !% \x => case p x of
 145 |     False => (Left x ** id)
 146 |     True => (Right x ** id)
 147 | 
 148 | 
 149 | 
 150 | namespace CartesianClosure
 151 |   ||| The following is the proof that for any container `c` there is an
 152 |   ||| isomorphism in `Cont` between `c` and `CartesianClosure UnitCont c`
 153 |   ||| This holds in any monoidal closed category: `X ≅ [I, X]`
 154 |   namespace StateIsomorphismProof
 155 |     stateToCartClosureFw : c =%> (CartesianClosure UnitCont c)
 156 |     stateToCartClosureFw = !% \cShp => (!% \() => (cShp ** \_ => Nothing)
 157 |                                        ** \(() ** cPos ** ItIsNothing) => cPos)
 158 | 
 159 |     stateToCartClosureBw : CartesianClosure UnitCont c =%> c
 160 |     stateToCartClosureBw = !% \l => (l.fwd () ** \cPos =>
 161 |       (() ** cPos ** maybeVoidIsNothing (l.bwd () cPos)))
 162 | 
 163 | 
 164 | ||| For a overview of this interaction from the categorical perspective, see
 165 | ||| the Poly book (https://arxiv.org/abs/2312.00990) (Section 6.3.4)
 166 | namespace CompositionTensorInteraction
 167 |   ||| Interaction between composition and tensor product
 168 |   ||| Swaps the operations, and middle two containers
 169 |   ||| Not an isomorphism!
 170 |   public export
 171 |   duoidal : (c >@ d) >< (e >@ f) =%> (c >< e) >@ (d >< f)
 172 |   duoidal = !% \((sc <| idxC), (se <| idxE)) =>
 173 |     ((sc, se) <| \(cp, ep) => (idxC cp, idxE ep) **
 174 |       \((cp, ep) ** (dp, fp)) => ((cp ** dp), (ep ** fp)))
 175 |   
 176 |   ||| Tensor product embeds into composition
 177 |   ||| A special case of `duoidal`
 178 |   public export
 179 |   tensorToComp : c >< f =%> c >@ f
 180 |   tensorToComp =   (rightUnitInv >< leftUnitInv)
 181 |                %>> duoidal {d=Scalar,e=Scalar}
 182 |                %>> (rightUnit >@ leftUnit)
 183 | 
 184 |   ||| Specific distributive law we need
 185 |   public export
 186 |   distribute : c >< e =%> s ->
 187 |     c >< (e >@ g) =%> s >@ g
 188 |   distribute f = (rightUnitInv >< id {c=e >@ g})
 189 |                %>> duoidal {d = Scalar}
 190 |                %>> (f >@ leftUnit)
 191 | 
 192 | 
 193 | namespace State
 194 |   ||| "State" as defined in https://arxiv.org/abs/2403.13001 and open games 
 195 |   |||
 196 |   |||       ┌─────────────┐
 197 |   |||       │             ├──► (x : c.Shp)
 198 |   |||       │    State    │
 199 |   |||       │             ├◄── c.Pos x
 200 |   |||       └─────────────┘
 201 |   public export
 202 |   State : Cont -> Type
 203 |   State c = Scalar =%> c
 204 | 
 205 |   ||| Given a shape of any container, state can be defined
 206 |   public export
 207 |   toState : (x : c.Shp) -> State c
 208 |   toState x = !% \() => (x ** \_ => ())
 209 | 
 210 |   public export
 211 |   fromState : State c -> c.Shp
 212 |   fromState f = f.fwd ()
 213 | 
 214 |   public export
 215 |   mapState : State c ->
 216 |     c =%> d ->
 217 |     State d
 218 |   mapState s f = s %>> f
 219 | 
 220 | namespace Costate
 221 |   ||| "Costate" as defined in https://arxiv.org/abs/2403.13001 and open games 
 222 |   |||
 223 |   |||                  ┌─────────────┐
 224 |   |||  (x : c.Shp)  ──►┤             │
 225 |   |||                  │   Costate   │
 226 |   |||     c.Pos x   ◄──┤             │
 227 |   |||                  └─────────────┘
 228 |   public export
 229 |   Costate : Cont -> Type
 230 |   Costate c = c =%> Scalar
 231 | 
 232 |   public export
 233 |   toCostate : ((x : c.Shp) -> c.Pos x) -> Costate c
 234 |   toCostate s = !% \x => (() ** \() => s x)
 235 | 
 236 |   public export
 237 |   fromCostate : Costate c -> (x : c.Shp) -> c.Pos x
 238 |   fromCostate f x = f.bwd x ()
 239 | 
 240 |   public export
 241 |   mapCostate : Costate d ->
 242 |     c =%> d ->
 243 |     Costate c
 244 |   mapCostate s f = f %>> s
 245 | 
 246 |   public export
 247 |   pairCostate : Costate c -> Costate d -> Costate (c >< d)
 248 |   pairCostate f g = (f >< g) %>> leftUnit {c=Scalar}
 249 |   
 250 | public export
 251 | fromNapCostateToState : Costate (Nap c.Shp) -> State c
 252 | fromNapCostateToState f = toState (f.bwd () ())
 253 | 
 254 | public export
 255 | fromStateToNapCostate : State c -> Costate (Nap c.Shp)
 256 | fromStateToNapCostate f = toCostate f.fwd
 257 | 
 258 | 
 259 | 
 260 | ||| Wraps a dependent lens `c =%> d`
 261 | ||| into one of type `c >@ Scalar =%> d >@ Scalar`
 262 | ||| Needed because `c >@ Scalar` isn't automatically reduced to `c`
 263 | public export
 264 | wrapIntoVector : c =%> d ->
 265 |   Tensor [c] =%> Tensor [d]
 266 | wrapIntoVector f = rightUnit %>> f %>> rightUnitInv
 267 | 
 268 | public export
 269 | wrapIntoMatrix : c >@ c' =%> d >@ d' ->
 270 |   Tensor [c, c'] =%> Tensor [d, d']
 271 | wrapIntoMatrix f =   (id >@ rightUnit)
 272 |                  %>> f
 273 |                  %>> (id >@ rightUnitInv)
 274 | 
 275 | ||| Wraps a dependent lens `c =%> d`
 276 | ||| into one of type `c >< Scalar =%> d >< Scalar`
 277 | ||| Needed because `c >< Scalar` isn't automatically reduced to `c`
 278 | public export
 279 | wrapIntoVectorHancock : c =%> d ->
 280 |   HancockTensor [c] =%> HancockTensor [d]
 281 | wrapIntoVectorHancock f = rightUnit %>> f %>> rightUnitInv
 282 | 
 283 | public export
 284 | pick : Pick c a =%> c
 285 | pick = !% \e => (shapeExt e ** index e)
 286 | 
 287 | ||| A lens from a container specialised to a shape to the container itself
 288 | public export
 289 | atShape : (s : c.Shp) -> At c s =%> c
 290 | atShape s = !% \() => (s ** id)
 291 | 
 292 | ||| A vector of positive length is a non-empty list
 293 | public export
 294 | vectToList1 : {k : Nat} -> Vect (S k) =%> List1
 295 | vectToList1 = !% \() => (k ** id)
 296 |     
 297 | 
 298 |   -- ||| Technically this is Unit, but hard to prove
 299 |   -- public export
 300 |   -- foldOverNaperianShapeComp : {shape : List Cont} ->
 301 |   --   (allNap : All IsNaperian shape) =>
 302 |   --   (Tensor shape).Shp
 303 |   -- foldOverNaperianShapeComp {shape = []} = ()
 304 |   -- foldOverNaperianShapeComp {allNap = ((MkIsNaperian pos) :: ns)}
 305 |   --   = () <| \_ => foldOverNaperianShapeComp
 306 |   -- 
 307 |   -- public export
 308 |   -- naperianHancockShape : {shape : List Cont} ->
 309 |   --   (allNap : All IsNaperian shape) =>
 310 |   --   (HancockTensor shape).Shp = Unit
 311 |   -- naperianHancockShape = believe_me ()
 312 |   -- 
 313 |   -- public export
 314 |   -- foldOverNaperianShapeHancock : {shape : List Cont} ->
 315 |   --   (allNap : All IsNaperian shape) =>
 316 |   --   (HancockTensor shape).Shp
 317 |   -- foldOverNaperianShapeHancock {shape = []} = ()
 318 |   -- foldOverNaperianShapeHancock {allNap = ((MkIsNaperian _) :: _)}
 319 |   --   = ((), foldOverNaperianShapeHancock)
 320 | 
 321 | 
 322 | -- public export
 323 | -- tensorIsNaperianShape : {shape : List Cont} ->
 324 | --   (allNap : All IsNaperian shape) =>
 325 | --   IsNaperian (Tensor shape)
 326 | -- tensorIsNaperianShape {shape = []} = MkIsNaperian ()
 327 | -- tensorIsNaperianShape {shape = (_ :: ss), allNap = ((MkIsNaperian pos) :: ns)}
 328 | --   = let tg = tensorIsNaperianShape {shape = ss} 
 329 | --     in ?tensorIsNaperianShape_rhs_1
 330 | --     --in rewrite naperianShpEq @{tg}
 331 | --     --in (rewrite (EmptyExtEq {c=(Nap pos)})
 332 | --     --in let tg = MkIsNaperian in ?tensorIsNaperianShape_rhs_2)
 333 | 
 334 | -- public export
 335 | -- transformToHancock : {shape : List Cont} ->
 336 | --   All IsNaperian shape =>
 337 | --   Tensor shape =%> HancockTensor shape
 338 | -- transformToHancock {shape = []} = id
 339 | -- transformToHancock {shape = (_ :: ss)} @{((MkIsNaperian pos) :: ns)}
 340 | --   = let f = (%!) (transformToHancock {shape = ss} @{ns})
 341 | --         (_ ** h) = f (foldOverNaperianShapeComp {shape=ss})
 342 | --     in !% \(() <| content) => (((), foldOverNaperianShapeHancock) **
 343 | --       \(p, fld) => (p ** ?hhh))
 344 | --       -- (((), rewrite -- foldOverNaperianShapeHancock {shape=ss} @{ns} in ()) **
 345 | --     --   \(p, fld) => (p ** ?bnn))
 346 | 
 347 | -- need to organise this
 348 | 
 349 | public export
 350 | handleEffect : Monad m =>
 351 |   (handler : (m <!> effect) =%> Scalar) ->
 352 |   (program : a =%> effect) ->
 353 |   m <!> a =%> Scalar
 354 | handleEffect handler program = !% \x =>
 355 |   let (ef ** nn) = (%! program) x
 356 |       (() ** rest) = (%! handler) ef
 357 |   in (() ** \() => do 
 358 |     e <- rest ()
 359 |     pure (nn e))
 360 | 
 361 | namespace BinTree
 362 |   public export
 363 |   inorderBackward : (b : BinTreeShape) ->
 364 |     Fin (numNodesAndLeaves b) ->
 365 |     BinTreePos b
 366 |   inorderBackward LeafS FZ = AtLeaf
 367 |   inorderBackward (NodeS lt rt) n with (strengthenN {m=numNodesAndLeaves lt} n)
 368 |      _ | Left p = GoLeft (inorderBackward lt p)
 369 |      _ | Right FZ = AtNode
 370 |      _ | Right (FS g) = GoRight (inorderBackward rt g)
 371 | 
 372 | 
 373 |   public export
 374 |   inorder : BinTree =%> List
 375 |   inorder = !% \b => (numNodesAndLeaves b ** inorderBackward b)
 376 | 
 377 | namespace BinTreeNode
 378 |   public export
 379 |   inorderBackward : (b : BinTreeShape) ->
 380 |     Fin (numNodes b) ->
 381 |     BinTreePosNode b
 382 |   inorderBackward (NodeS lt rt) n with (strengthenN {m=numNodes lt} n)
 383 |     _ | Left p = GoLeft (inorderBackward lt p)
 384 |     _ | Right FZ = AtNode
 385 |     _ | Right (FS g) = GoRight (inorderBackward rt g)
 386 | 
 387 |   ||| Traverses a binary tree container in order, producing a list container
 388 |   public export
 389 |   inorder : BinTreeNode =%> List
 390 |   inorder = !% \b => (numNodes b ** inorderBackward b)
 391 | 
 392 |   -- Need to do some rewriting for preorder
 393 |   public export
 394 |   preorderBinTreeNode : (b : BinTreeShape) ->
 395 |     Fin (numNodes b) -> BinTreePosNode b
 396 |   preorderBinTreeNode (NodeS lt rt) x = ?preorderBinTreeNode_rhs_1
 397 |   --preorderBinTreeNode (NodeS lt rt) n with (strengthenN {m=numNodes lt} n)
 398 |   --  _ | Left p = ?whl
 399 |   --  _ | Right FZ = ?whn
 400 |   --  _ | Right (FS g) = ?whr
 401 | 
 402 | namespace BinTreeLeaf
 403 |   public export
 404 |   inorderBackward : (b : BinTreeShape) ->
 405 |     Fin (numLeaves b) ->
 406 |     BinTreePosLeaf b
 407 |   inorderBackward LeafS 0 = AtLeaf
 408 |   inorderBackward (NodeS lt rt) i with (strengthenN {m=numLeaves lt} i)
 409 |     _ | (Left indLeft) = GoLeft (inorderBackward lt indLeft)
 410 |     _ | (Right indRight) = GoRight (inorderBackward rt indRight)
 411 | 
 412 |   public export
 413 |   inorder : BinTreeLeaf =%> List
 414 |   inorder = !% \b => (numLeaves b ** inorderBackward b)
 415 | 
 416 | -- public export
 417 | -- traverseLeaf : (x : BinTreeShape) -> FinBinTreeLeaf x -> Fin (numLeaves x)
 418 | -- traverseLeaf LeafS Done = FZ
 419 | -- traverseLeaf (NodeS lt rt) (GoLeft x) = weakenN (numLeaves rt) (traverseLeaf lt x)
 420 | -- traverseLeaf (NodeS lt rt) (GoRight x) = shift (numLeaves lt) (traverseLeaf rt x)
 421 | -- 
 422 | 
 423 | public export
 424 | vectToList : {n : Nat} -> Vect n =%> List
 425 | vectToList = !% \() => (n ** id)
 426 | 
 427 | public export
 428 | maybeToList : Maybe =%> List
 429 | maybeToList = !% \b => case b of 
 430 |   False => (0 ** absurd)
 431 |   True => (1 ** \_ => ())
 432 |