0 | module Data.Container.Base.Monoid.Instances
  1 |
  2 | import Data.Container.Base.Object.Definition
  3 | import Data.Container.Base.Extension.Definition
  4 | import Data.Container.Base.Morphism.Definition
  5 | import Data.Container.Base.Product.Definition
  6 | import Data.Container.Base.Properties.Definition
  7 |
  8 | import Data.Container.Base.Object.Instances
  9 | import Data.Container.Base.Extension.Instances
 10 | import Data.Container.Base.Morphism.Instances
 11 | import Data.Container.Base.Monoid.Definition
 12 | import Data.Container.Base.Properties.Instances
 13 |
 14 | import Data.Container.Base.TreeUtils
 15 |
 16 | import Data.Fin.Split
 17 | import Data.Layout
 18 | import Data.Functor.Algebra
 19 |
 20 | import Misc
 21 |
 22 | export
 23 | TensorMonoid Maybe where
 24 |   tensorN = toState True
 25 |   tensorM = !% \(b1, b2) => (b1 && b2 ** \bb => case b1 of
 26 |     True => ((), if b2 then bb else absurd bb)
 27 |     False => absurd bb)
 28 |
 29 | ||| Chaining computation
 30 | ||| Different from ordinary `Either` in that both variables are of the same type
 31 | export
 32 | TensorMonoid Either where
 33 |   tensorN = toState True
 34 |   tensorM = !% \(b1, b2) => (b1 && b2 ** \() => ((), ()))
 35 |
 36 | ||| Corresponds to the Applicative instance in `Prelude.Types`
 37 | ||| It behaves like a cartesian product, but compared to `Prelude.Types`
 38 | ||| applicative this is layout-aware
 39 | export
 40 | TensorMonoid List where
 41 |   tensorN = toState 1
 42 |   tensorM = !% \(n, m) => (n * m ** splitFinProd DefaultLayoutOrder) 
 43 |
 44 | export
 45 | SeqMonoid List where
 46 |   seqM = !% \(n <| contentM) => (sum contentM ** splitFinProdDep contentM)
 47 |
 48 | {--
 49 | It is usually said that List has two applicative structures: one defined above,
 50 | and another one defined by `zipList` (Section 3 of 
 51 | https://www.staff.city.ac.uk/~ross/papers/Constructors.pdf). However, such
 52 | a definition relies on the laziness of the underlying programming language
 53 | and implicitly recast the type not to `List` but `CoList` (sometimes called 
 54 | `LazyList`), i.e. a list with potentially infinite number of elements. This permits defining `pure` and showing that applicative laws hold. However, since Idris is a strict language, List is not equal to CoList, and we cannot lawfully
 55 | make `List` an applicative functor. More precisely, the following is not a valid applicative instance, because unital laws do not hold:
 56 |
 57 | Applicative List where
 58 |   pure a = [a]
 59 |   fs <*> xs = uncurry ($) <$> listZip fs xs
 60 | --}   
 61 |
 62 |
 63 | ||| Covers pairs, vectors, streams, grids, among others
 64 | ||| For vectors produces a `zip` operation
 65 | export
 66 | IsNaperian c => TensorMonoid c where
 67 |   tensorN @{(Via _)} = toState ()
 68 |   tensorM @{(Via _)} = !% \((), ()) => (() ** \i => (i, i))
 69 |
 70 | public export
 71 | [compositeTensorMonoid]
 72 | TensorMonoid c => TensorMonoid d => TensorMonoid (c >@ d) where
 73 |   tensorN = leftUnitInv %>> (tensorN >@ tensorN)
 74 |   tensorM = duoidal %>> (tensorM >@ tensorM)
 75 |
 76 | ||| When a container `c` is Naperian, then `c >< c` is isomorphic to `c >@ c`
 77 | ||| Meaning this interface follows directly
 78 | ||| Vectors also form a *graded* monad, which isn't implemented here
 79 | export
 80 | IsNaperian c => SeqMonoid c where
 81 |   seqM @{Via pos} = compToTensor {d=c} %>> tensorM
 82 |
 83 |
 84 | ||| Tensor preserves TensorMonoid/Applicative
 85 | public export
 86 | tensorPreservesTensorMonoid : {shape : List Cont} ->
 87 |   (allAppl : All TensorMonoid shape) =>
 88 |    TensorMonoid (Tensor shape)
 89 | tensorPreservesTensorMonoid {shape = []} = %search
 90 | tensorPreservesTensorMonoid {shape = (_ :: _), allAppl = (p :: _)}
 91 |   = compositeTensorMonoid @{p} @{tensorPreservesTensorMonoid}
 92 |
 93 |
 94 | ||| experiment, does this work?
 95 | diagonalAroundMiddle : IsNaperian c =>
 96 |   (f : c >@ c =%> c) ->
 97 |   c >@ d >@ c =%> c >@ d
 98 |
 99 |
100 | public export
101 | join : SeqMonoid c =>
102 |   Tensor [c, c] =%> Tensor [c]
103 | join =   (id >@ rightUnit)
104 |      %>> seqM
105 |      %>> rightUnitInv
106 |
107 | public export
108 | cojoin : SeqComonoid c =>
109 |   Tensor [c] =%> Tensor [c, c]
110 | cojoin = rightUnit
111 |        %>> seqComult
112 |        %>> (id >@ rightUnitInv)
113 |
114 | public export
115 | diagonal : IsNaperian c =>
116 |   Tensor [c, c] =%> Tensor [c]
117 | diagonal = join
118 |
119 | public export
120 | codiagonal : TensorMonoid c =>
121 |   Tensor [c] =%> Tensor [c, c]
122 | codiagonal = ?codiagonalTensorMonoid_rhs
123 |
124 |
125 | namespace BinTreeUtils
126 |   public export
127 |   pairBTreeShapes : BinTreeShape -> BinTreeShape -> BinTreeShape
128 |   pairBTreeShapes LeafS LeafS
129 |     = LeafS
130 |   pairBTreeShapes LeafS (NodeS ltb rtb)
131 |     = NodeS (pairBTreeShapes LeafS ltb) (pairBTreeShapes LeafS rtb)
132 |   pairBTreeShapes (NodeS lta rta) LeafS
133 |     = NodeS (pairBTreeShapes lta LeafS) (pairBTreeShapes rta LeafS)
134 |   pairBTreeShapes (NodeS lta rta) (NodeS ltb rtb)
135 |     = NodeS (pairBTreeShapes lta ltb) (pairBTreeShapes rta rtb)
136 |
137 |   -- needs to be checked if this is right...  some previous related code at
138 |   -- git show adf4ad5:src/Data/Container/Applicative/Instances.idr
139 |   public export
140 |   pairBTreePos : {sh1, sh2 : BinTreeShape} ->
141 |     BinTreePos (pairBTreeShapes sh1 sh2) -> (BinTreePos sh1, BinTreePos sh2)
142 |   pairBTreePos {sh1 = LeafS, sh2 = LeafS} AtLeaf
143 |     = (AtLeaf, AtLeaf)
144 |   pairBTreePos {sh1 = LeafS, sh2 = (NodeS ltb rtb)} p
145 |     = (AtLeaf, case p of
146 |         AtNode => AtNode
147 |         GoLeft posL => GoLeft $ snd (pairBTreePos posL)
148 |         GoRight posR => GoRight $ snd (pairBTreePos posR))
149 |   pairBTreePos {sh1 = (NodeS lta rta), sh2 = LeafS} p
150 |     = (case p of
151 |         AtNode => AtNode
152 |         GoLeft posL => GoLeft $ fst (pairBTreePos posL)
153 |         GoRight posR => GoRight $ fst (pairBTreePos posR), AtLeaf)
154 |   pairBTreePos {sh1 = (NodeS lta rta), sh2 = (NodeS ltb rtb)} p
155 |     = case p of
156 |         AtNode => (AtNode, AtNode)
157 |         GoLeft posL => let (pl, pr) = pairBTreePos posL
158 |                        in (GoLeft $ pl, GoLeft $ pr)
159 |         GoRight posR => let (pl, pr) = pairBTreePos posR
160 |                        in (GoRight $ pl, GoRight $ pr)
161 |   
162 |   public export
163 |   pairBTreeLeafPos : {sh1, sh2 : BinTreeShape} ->
164 |     BinTreePosLeaf (pairBTreeShapes sh1 sh2) ->
165 |     (BinTreePosLeaf sh1, BinTreePosLeaf sh2)
166 |   pairBTreeLeafPos {sh1 = LeafS, sh2 = LeafS} AtLeaf
167 |     = (AtLeaf, AtLeaf)
168 |   pairBTreeLeafPos {sh1 = LeafS, sh2 = (NodeS ltb rtb)} p
169 |     = (AtLeaf, case p of
170 |         GoLeft posL => GoLeft $ snd (pairBTreeLeafPos posL)
171 |         GoRight posR => GoRight $ snd (pairBTreeLeafPos posR))
172 |   pairBTreeLeafPos {sh1 = (NodeS lta rta), sh2 = LeafS} p
173 |     = (case p of
174 |         GoLeft posL => GoLeft $ fst (pairBTreeLeafPos posL)
175 |         GoRight posR => GoRight $ fst (pairBTreeLeafPos posR), AtLeaf)
176 |   pairBTreeLeafPos {sh1 = (NodeS lta rta), sh2 = (NodeS ltb rtb)} p
177 |     = case p of
178 |         GoLeft posL => let (pl, pr) = pairBTreeLeafPos posL
179 |                        in (GoLeft $ pl, GoLeft $ pr)
180 |         GoRight posR => let (pl, pr) = pairBTreeLeafPos posR
181 |                        in (GoRight $ pl, GoRight $ pr)
182 |
183 | export
184 | TensorMonoid BinTree where
185 |   tensorN = toState LeafS
186 |   tensorM = !% \(sh1, sh2) => (pairBTreeShapes sh1 sh2 ** pairBTreePos)
187 |
188 | export
189 | TensorMonoid BinTreeLeaf where
190 |   tensorN = toState LeafS
191 |   tensorM = !% \(sh1, sh2) => (pairBTreeShapes sh1 sh2 ** pairBTreeLeafPos)
192 |
193 | -- Note, there is no TensorMonoid/Applicative instance for BinTreeNode
194 | -- There exists one for infinite trees, but not finite ones
195 |
196 | reduce : {c : Cont} -> Algebra (Ext c) a =>
197 |   Ext c a -> Ext Scalar a
198 | reduce x = () <| \() => reduce x
199 |
200 | public export
201 | dotWith : {cont : Cont} -> TensorMonoid cont => Algebra (Ext cont) c =>
202 |   (a -> b -> c) ->
203 |   Ext cont a -> Ext cont b -> Ext Scalar c
204 | dotWith f ea eb = reduce $ uncurry f <$> liftA2Ext ea eb
205 |