
  0 | module Data.Container.Base.Product.Interfaces
  1 | 
  2 | import public Data.List.Quantifiers
  3 | 
  4 | import Data.Container.Base.Object.Definition
  5 | import Data.Container.Base.Morphism.Definition
  6 | import Data.Container.Base.Extension.Definition
  7 | import Data.Container.Base.Product.Definitions
  8 | import Data.Container.Base.Object.Instances
  9 | import Data.Container.Base.Morphism.Instances
 10 | 
 11 | ||| Its extension is an applicative functor
 12 | ||| All Naperian containers, BinTree, BinTreeLeaf, List, Maybe,...
 13 | public export
 14 | interface TensorMonoid (0 c : Cont) where
 15 |   tensorN : Scalar =%> c
 16 |   tensorM : c >< c =%> c
 17 | 
 18 | public export
 19 | interface TensorComonoid (0 c : Cont) where
 20 |   tensorCounit : c =%> Scalar
 21 |   tensorComult : c =%> c >< c
 22 | 
 23 | ||| Its extension is a monad
 24 | ||| Just as Applicative => Monad, here TensorMonoid => SeqMonoid
 25 | public export
 26 | interface TensorMonoid c => SeqMonoid (0 c : Cont) where
 27 |   seqM : c >@ c =%> c
 28 | 
 29 | ||| These are directed containers, a.k.a. categories
 30 | ||| Does this interface constraint follow analogously?
 31 | public export
 32 | interface TensorComonoid c => SeqComonoid (0 c : Cont) where
 33 |   seqComult : c =%> c >@ c
 34 | 
 35 | public export
 36 | interface CoprodMonoid (0 c : Cont) where
 37 |   plusN : Empty =%> c
 38 |   plusM : c >+< c =%> c
 39 | 
 40 | ||| Its extension is an Alternative?
 41 | public export
 42 | interface ProdMonoid (0 c : Cont) where
 43 |   prodN : UnitCont =%> c
 44 |   prodM : c >*< c =%> c
 45 | 
 46 | public export
 47 | pairExtensions : Ext c a -> Ext d b -> Ext (c >< d) (a, b)
 48 | pairExtensions (shapeC <| indexC) (shapeD <| indexD)
 49 |   = (shapeC, shapeD) <| \(posC, posD) => (indexC posC, indexD posD)
 50 | 
 51 | public export
 52 | liftA2Ext : TensorMonoid c => Ext c a -> Ext c b -> Ext c (a, b)
 53 | liftA2Ext aExt bExt = extMap tensorM $ pairExtensions aExt bExt
 54 | 
 55 | public export
 56 | TensorMonoid c => Applicative (Ext c) where
 57 |   pure x = tensorN.fwd () <| const x
 58 |   fExt <*> aExt = uncurry ($) <$> liftA2Ext fExt aExt
 59 | 
 60 | public export
 61 | [FromSeq] SeqMonoid c => Applicative (Ext c) where
 62 |   pure x = tensorN.fwd () <| const x
 63 |   (f <| f') <*> (x <| x') = ?notAThing
 64 | 
 65 | public export
 66 | SeqMonoid c => Monad (Ext c) using FromSeq where
 67 |   join (a <| b) = let (q1 ** q2) = (%! seqM) (a <| shapeExt . b)
 68 |                   in q1 <| ((\xx => (b xx.fst).index xx.snd) . q2)
 69 | 
 70 | public export
 71 | [FromProd] ProdMonoid c => Applicative (Ext c) where
 72 |   pure x = prodN.fwd () <| const x
 73 |   (<*>) = ?notAThing2
 74 | 
 75 | public export
 76 | ProdMonoid c => Alternative (Ext c) using FromProd where
 77 |   empty = let (p1 ** p2) = (%! prodN) () in p1 <| absurd . p2
 78 |   (<|>) (a <| a') (b <| b') =
 79 |     let (m1 ** m2) = (%! prodM) (a, b) in m1 <| either a' b' . m2
 80 |