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