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 @{(MkIsNaperian _)} = toState ()
 68 |   tensorM @{(MkIsNaperian _)} = !% \((), ()) => (() ** \i => (i, i))
 69 |
 70 | ||| When a container `c` is Naperian, then `c >< c` is isomorphic to `c >@ c`
 71 | ||| Meaning this interface follows directly
 72 | ||| Vectors also form a *graded* monad, which isn't implemented here
 73 | export
 74 | IsNaperian c => SeqMonoid c where
 75 |   seqM @{MkIsNaperian pos} = compToTensor {d=c} %>> tensorM
 76 |
 77 |
 78 | ||| experiment, does this work?
 79 | diagonalAroundMiddle : IsNaperian c =>
 80 |   (f : c >@ c =%> c) ->
 81 |   c >@ d >@ c =%> c >@ d
 82 |
 83 |
 84 | public export
 85 | join : SeqMonoid c =>
 86 |   Tensor [c, c] =%> Tensor [c]
 87 | join =   (id >@ rightUnit)
 88 |      %>> seqM
 89 |      %>> rightUnitInv
 90 |
 91 | public export
 92 | cojoin : SeqComonoid c =>
 93 |   Tensor [c] =%> Tensor [c, c]
 94 | cojoin = rightUnit
 95 |        %>> seqComult
 96 |        %>> (id >@ rightUnitInv)
 97 |
 98 | public export
 99 | diagonal : IsNaperian c =>
100 |   Tensor [c, c] =%> Tensor [c]
101 | diagonal = join
102 |
103 | public export
104 | codiagonal : TensorMonoid c =>
105 |   Tensor [c] =%> Tensor [c, c]
106 | codiagonal = ?cojoinn
107 |
108 |
109 | namespace BinTreeUtils
110 |   public export
111 |   pairBTreeShapes : BinTreeShape -> BinTreeShape -> BinTreeShape
112 |   pairBTreeShapes LeafS LeafS
113 |     = LeafS
114 |   pairBTreeShapes LeafS (NodeS ltb rtb)
115 |     = NodeS (pairBTreeShapes LeafS ltb) (pairBTreeShapes LeafS rtb)
116 |   pairBTreeShapes (NodeS lta rta) LeafS
117 |     = NodeS (pairBTreeShapes lta LeafS) (pairBTreeShapes rta LeafS)
118 |   pairBTreeShapes (NodeS lta rta) (NodeS ltb rtb)
119 |     = NodeS (pairBTreeShapes lta ltb) (pairBTreeShapes rta rtb)
120 |
121 |   -- needs to be checked if this is right...  some previous related code at
122 |   -- git show adf4ad5:src/Data/Container/Applicative/Instances.idr
123 |   public export
124 |   pairBTreePos : {sh1, sh2 : BinTreeShape} ->
125 |     BinTreePos (pairBTreeShapes sh1 sh2) -> (BinTreePos sh1, BinTreePos sh2)
126 |   pairBTreePos {sh1 = LeafS, sh2 = LeafS} AtLeaf
127 |     = (AtLeaf, AtLeaf)
128 |   pairBTreePos {sh1 = LeafS, sh2 = (NodeS ltb rtb)} p
129 |     = (AtLeaf, case p of
130 |         AtNode => AtNode
131 |         GoLeft posL => GoLeft $ snd (pairBTreePos posL)
132 |         GoRight posR => GoRight $ snd (pairBTreePos posR))
133 |   pairBTreePos {sh1 = (NodeS lta rta), sh2 = LeafS} p
134 |     = (case p of
135 |         AtNode => AtNode
136 |         GoLeft posL => GoLeft $ fst (pairBTreePos posL)
137 |         GoRight posR => GoRight $ fst (pairBTreePos posR), AtLeaf)
138 |   pairBTreePos {sh1 = (NodeS lta rta), sh2 = (NodeS ltb rtb)} p
139 |     = case p of
140 |         AtNode => (AtNode, AtNode)
141 |         GoLeft posL => let (pl, pr) = pairBTreePos posL
142 |                        in (GoLeft $ pl, GoLeft $ pr)
143 |         GoRight posR => let (pl, pr) = pairBTreePos posR
144 |                        in (GoRight $ pl, GoRight $ pr)
145 |   
146 |   public export
147 |   pairBTreeLeafPos : {sh1, sh2 : BinTreeShape} ->
148 |     BinTreePosLeaf (pairBTreeShapes sh1 sh2) ->
149 |     (BinTreePosLeaf sh1, BinTreePosLeaf sh2)
150 |   pairBTreeLeafPos {sh1 = LeafS, sh2 = LeafS} AtLeaf
151 |     = (AtLeaf, AtLeaf)
152 |   pairBTreeLeafPos {sh1 = LeafS, sh2 = (NodeS ltb rtb)} p
153 |     = (AtLeaf, case p of
154 |         GoLeft posL => GoLeft $ snd (pairBTreeLeafPos posL)
155 |         GoRight posR => GoRight $ snd (pairBTreeLeafPos posR))
156 |   pairBTreeLeafPos {sh1 = (NodeS lta rta), sh2 = LeafS} p
157 |     = (case p of
158 |         GoLeft posL => GoLeft $ fst (pairBTreeLeafPos posL)
159 |         GoRight posR => GoRight $ fst (pairBTreeLeafPos posR), AtLeaf)
160 |   pairBTreeLeafPos {sh1 = (NodeS lta rta), sh2 = (NodeS ltb rtb)} p
161 |     = case p of
162 |         GoLeft posL => let (pl, pr) = pairBTreeLeafPos posL
163 |                        in (GoLeft $ pl, GoLeft $ pr)
164 |         GoRight posR => let (pl, pr) = pairBTreeLeafPos posR
165 |                        in (GoRight $ pl, GoRight $ pr)
166 |
167 | export
168 | TensorMonoid BinTree where
169 |   tensorN = toState LeafS
170 |   tensorM = !% \(sh1, sh2) => (pairBTreeShapes sh1 sh2 ** pairBTreePos)
171 |
172 | export
173 | TensorMonoid BinTreeLeaf where
174 |   tensorN = toState LeafS
175 |   tensorM = !% \(sh1, sh2) => (pairBTreeShapes sh1 sh2 ** pairBTreeLeafPos)
176 |
177 | -- Note, there is no TensorMonoid/Applicative instance for BinTreeNode
178 | -- There exists one for infinite trees, but not finite ones
179 |
180 | reduce : {c : Cont} -> Algebra (Ext c) a =>
181 |   Ext c a -> Ext Scalar a
182 | reduce x = () <| \() => reduce x
183 |
184 | public export
185 | dotWith : {cont : Cont} -> TensorMonoid cont => Algebra (Ext cont) c =>
186 |   (a -> b -> c) ->
187 |   Ext cont a -> Ext cont b -> Ext Scalar c
188 | dotWith f ea eb = reduce $ uncurry f <$> liftA2Ext ea eb
189 |