replace AllApplicative by tensor monoid

pack.toml

@@ -11,4 +11,5 @@ ipkg = "tensortype-examples.ipkg"
 # [custom.all.tensortype-tests]
 # type = "local"
 # path = "tests"
-# ipkg = "tensortype-tests.ipkg"
+# ipkg = "tensortype-tests.ipkg"
+

src/Data/Container/Applicative/Definition.idr

@@ -31,31 +31,17 @@ public export
 (.Pos) : (c : ContA) -> c.Shp -> Type
 (.Pos) c sh = (GetC c) .Pos sh
 
--- alternative method of using applicative instances, not sure yet if this is better
-public export
-data AllApplicative : List Cont -> Type where
-  Nil : AllApplicative []
-  Cons : (firstAppl : Applicative (Ext c)) =>
-    (restAppl : AllApplicative cs) =>
-    AllApplicative (c :: cs)
-
-
--- is there a better way?
-%hint
-public export
-oneToTwoAppl : AllApplicative [c] => AllApplicative [c, c]
-oneToTwoAppl @{Cons} = Cons
 
 
 
--- ||| This states a list version of 
+-- ||| This states a list version of
 -- ||| Ext c2 . Ext c1 = Ext (c2 . c1)
 -- public export
 -- ToContainerComp : {conts : List ContA} ->
 --   composeExtensionsA conts a -> Ext (composeContainersA conts) a
 -- ToContainerComp {conts = []} ce = ce
 -- ToContainerComp {conts = [c]} ce = ce
--- ToContainerComp {conts = (c :: d :: cs)} (Shp <| idx) = 
+-- ToContainerComp {conts = (c :: d :: cs)} (Shp <| idx) =
 --   let rst = (ToContainerComp {conts=(d :: cs)}) . idx
 --   in (Shp <| shapeExt . rst) <| (\(cp ** fsh) => index (rst cp) fsh)
 
@@ -75,21 +61,21 @@ oneToTwoAppl @{Cons} = Cons
 --   (f : a -> b) -> composeExtensionsA conts a -> composeExtensionsA conts b
 -- mapcomposeExtensionsA {conts = []} f e = f <$> e
 -- mapcomposeExtensionsA {conts = ((# c) :: cs)} f e = mapcomposeExtensionsA f <$> e
--- 
+--
 -- public export
 -- [FCE] {conts : List ContA} -> Functor (composeExtensionsA conts) where
 --   map f ce = ?vnn -- mapcomposeExtensionsA
--- 
+--
 -- testTT : {c : ContA} -> (f : String -> Int) -> composeExtensionsA [c] String -> composeExtensionsA [c] Int
 -- testTT f = map @{FCE {conts=[c]}} f
--- 
+--
 -- public export
 -- compExtReplicate : {conts : List ContA} ->
 --   a -> composeExtensionsA conts a
 -- compExtReplicate {conts = []} a = pure a
 -- compExtReplicate {conts = ((#) _ {applPrf} :: _)} a
 --   = compExtReplicate <$> pure a
--- 
+--
 -- public export
 -- compExtLiftA2 : {conts : List ContA} ->
 --   composeExtensionsA conts a ->

src/Data/Container/Interfaces.idr

@@ -0,0 +1,63 @@
+module Data.Container.Interfaces
+
+import Data.Container.Object.Instances
+import Data.Container.Object.Definition
+import Data.Container.Products
+import Data.Container.Extension.Definition
+import public Data.Container.Morphism.Definition
+
+import public Data.List.Quantifiers
+
+public export
+interface TensorMonoid (0 c : Cont) where
+  tensorN : Scalar =%> c
+  tensorM : (c >< c) =%> c
+
+public export
+interface SeqMonoid (0 c : Cont) where
+  seqN : Scalar =%> c
+  seqM : (c >@ c) =%> c
+
+public export
+interface CoprodMonoid (0 c : Cont) where
+  plusN : Empty =%> c
+  plusM : (c >+< c) =%> c
+
+public export
+interface ProdMonoid (0 c : Cont) where
+  prodN : UnitCont =%> c
+  prodM : (c >*< c) =%> c
+
+public export
+AllApplicative : List Cont -> Type
+AllApplicative = All TensorMonoid
+
+public export
+(tt : TensorMonoid c) => Applicative (Ext c) where
+  pure x = (tensorN @{tt}).fwd () <| (const x)
+  (f <| f') <*> (x <| x') =
+    let (q1 ** qq) = (%! tensorM @{tt}) (f, x)
+    in q1 <| (\z => let (p1, p2) = qq z in f' p1 (x' p2))
+
+public export
+[FromSeq] (tt : SeqMonoid c) => Applicative (Ext c) where
+  pure x = seqN.fwd () <| (const x)
+  (f <| f') <*> (x <| x') = ?notAThing
+
+public export
+(tt : SeqMonoid c) => Monad (Ext c) using FromSeq where
+  join (a <| b) = let (q1 ** q2) = (%! seqM @{tt}) (a <| shapeExt . b)
+                   in q1 <| ((\xx => (b xx.fst).index xx.snd) . q2)
+
+public export
+[FromProd] (tt : ProdMonoid c) => Applicative (Ext c) where
+  pure x = prodN.fwd () <| const x
+  (<*>) = ?notAThing2
+
+
+public export
+(tt : ProdMonoid c) => Alternative (Ext c) using FromProd where
+  empty = let (p1 ** p2) = (%! prodN @{tt}) () in p1 <| absurd . p2
+  (<|>) (a <| a') (b <| b') =
+    let (m1 ** m2) = (%! prodM @{tt}) (a, b) in m1 <| either a' b' . m2
+

src/Data/Container/Morphism/Definition.idr

@@ -5,7 +5,6 @@ import Data.DPair
 import Data.Container.Object.Definition
 import Misc
 
-
 {-------------------------------------------------------------------------------
 Two different types of morphisms:
 dependent lenses, and dependent charts
@@ -37,11 +36,14 @@ namespace DependentLenses
   (%!) : c1 =%> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))
   (%!) (!% f) x = f x
 
-
+  public export
+  (.fwd) : c1 =%> c2 -> c1.Shp -> c2.Shp
+  (.fwd) x y = ((%! x) y).fst
+
   ||| Composition of dependent lenses
   public export
   compDepLens : a =%> b -> b =%> c -> a =%> c
-  compDepLens (!% f) (!% g) = !% \x => let (b ** kb) = f x 
+  compDepLens (!% f) (!% g) = !% \x => let (b ** kb) = f x
                                            (c ** kc) = g b
                                        in (c ** kb . kc)
   public export
@@ -64,10 +66,10 @@ namespace DependentCharts
   public export
   (&!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
   (&!) (!& f) x = f x
-  
+
   public export
   compDepChart : a =&> b -> b =&> c -> a =&> c
-  compDepChart (!& f) (!& g) = !& \x => let (b ** kb) = f x 
+  compDepChart (!& f) (!& g) = !& \x => let (b ** kb) = f x
                                             (c ** kc) = g b
                                         in (c ** kc . kb)
 
@@ -104,7 +106,7 @@ namespace Cartesian
   public export
   (:&) : c1 =:> c2 -> c1 =&> c2
   (:&) (!: f) = !& \x => let (y ** ky) = f x in (y ** forward ky)
-    
+
 ||| Pairing of all possible combinations of inputs to a particular lens
 public export
 lensInputs : {c, d : Cont} -> c =%> d -> Cont
@@ -116,10 +118,10 @@ lensInputs l = (x : c.Shp) !> d.Pos (fst ((%!) l x))
 val : Cont -> Type -> Cont
 val (shp !> pos) r = (s : shp) !> (pos s -> r)
 
--- Chart -> DLens morphism 
+-- Chart -> DLens morphism
 -- Tangent bundle to Contanget bundle, effectively
 valContMap : {c1, c2 : Cont} -> {r : Type}
   ->  (f : c1 =&> c2)
   ->  (c1 `val` r) =%> (c2 `val` r)
 valContMap {c1=(shp !> pos)} {c2=(shp' !> pos')} (!& f)
-  = !% \x => let (y ** ky) = f x in (y ** (. ky))
+  = !% \x => let (y ** ky) = f x in (y ** (. ky))

src/Data/Container/Object/Implementations.idr

@@ -0,0 +1,17 @@
+module Data.Container.Object.Implementations
+
+import Data.Container.Interfaces
+import Data.Container.Object.Definition
+import Data.Container.Object.Instances
+import Data.Fin
+import Data.Fin.Split
+
+export
+TensorMonoid List where
+  tensorN = !% \x => (0 ** absurd)
+  tensorM = !% \(x1, x2) => (x1 * x2 ** splitProd)
+
+export
+TensorMonoid (Vect n) where
+  tensorN = !% \x => (() ** const ())
+  tensorM = !% \x => (() ** (\x => (x, x)))

src/Data/Container/Object/Instances.idr

@@ -61,7 +61,7 @@ MaybeTwo = (b : Bool) !> (if b then Fin 2 else Void)
 public export
 List : Cont
 List = (n : Nat) !> Fin n
-  
+
 ||| Vect, container of a fixed/known number of things
 ||| As a polynomial functor: F(X) = X^n
 public export
@@ -79,15 +79,15 @@ Stream = (_ : Unit) !> Nat
 public export
 BinTree : Cont
 BinTree = (b : BinTreeShape) !> BinTreePos b
-  
+
 ||| Container of things stored at nodes of a binary tree
-||| As a polynomial functor: F(X) = 1 + X + 2X^2 + 5X^3 + 
+||| As a polynomial functor: F(X) = 1 + X + 2X^2 + 5X^3 +
 public export
 BinTreeNode : Cont
 BinTreeNode = (b : BinTreeShape) !> BinTreePosNode b
-  
+
 ||| Container of things stored at leaves of a binary tree
-||| As a polynomial functor: F(X) = X + X^2 + 2X^3 + 5X^4 + 
+||| As a polynomial functor: F(X) = X + X^2 + 2X^3 + 5X^4 +
 public export
 BinTreeLeaf : Cont
 BinTreeLeaf = (b : BinTreeShape) !> BinTreePosLeaf b
@@ -100,7 +100,7 @@ Tensor = foldr (>@) Scalar
 
 -- TODO what is "Tensor" with hancock product? with cartesian product?
 -- TODO duoidal structure between with hancock product and composition
-  
+
 ||| Every lens gives rise to a container
 ||| The set of shapes is the lens itself
 ||| The set of positions is the inputs to the lens
@@ -126,12 +126,12 @@ public export
 Const : Type -> Type -> Cont
 Const a b = (_ : a) !> b
 
-||| Constant container with a single shape  
+||| Constant container with a single shape
 ||| Naperian container
 ||| As a polynomial functor: F(X) = X^b
 public export
 Nap : Type -> Cont
 Nap b = Const Unit b
 
--- Some more examples that require the Applicative constraint can be found in 
+-- Some more examples that require the Applicative constraint can be found in
 -- `Data.Container.Object.Applicative`

src/Data/Container/Products.idr

@@ -23,7 +23,7 @@ c1 >*< c2 = ((s, s') : (c1.Shp, c2.Shp)) !> Either (c1.Pos s) (c2.Pos s')
 ||| Monoid with CUnit
 public export
 (><) : Cont -> Cont -> Cont
-c1 >< c2 = ((s, s') : (c1.Shp, c2.Shp)) !> (c1.Pos s, c2.Pos s')
+c1 >< c2 = (ss : (c1.Shp, c2.Shp)) !> (c1.Pos (fst ss), c2.Pos (snd ss))
 
 
 ||| Coproduct of containers
@@ -47,7 +47,7 @@ c @> d = (ex : Ext d c.Shp) !> (dp : d.Pos (shapeExt ex) ** c.Pos (index ex dp))
 
 
 ||| Derivative of a container
-||| Given c=(Shp !> pos) the derivative can be thought of as 
+||| Given c=(Shp !> pos) the derivative can be thought of as
 ||| a shape s : Shp, a distinguished position p : pos s, and the set of *all other positions*
 public export
 Deriv : (c : Cont) ->