From 0457421424378f930db73420eb60de3a6e37149c Mon Sep 17 00:00:00 2001
From: Andre Videla <me@andrevidela.com>
Date: Tue, 13 Jan 2026 23:54:34 +0000
Subject: [PATCH 1/2] replace AllApplicative by tensor monoid

---
 pack.toml                                     |   3 +-
 src/Data/Container/Applicative/Definition.idr |  26 +----
 src/Data/Container/Interfaces.idr             |  63 +++++++++++
 src/Data/Container/Morphism/Definition.idr    |  18 +--
 src/Data/Container/Object/Implementations.idr |  16 +++
 src/Data/Container/Object/Instances.idr       |  16 +--
 src/Data/Container/Products.idr               |   4 +-
 src/Data/Tensor/Tensor.idr                    | 105 +++++++++---------
 src/Data/Tensor/Utils.idr                     |  40 +++----
 src/NN/Architectures/Affine.idr               |  10 +-
 src/NN/Architectures/MLP.idr                  |   9 +-
 .../Architectures/Transformer/Attention.idr   |  25 +++--
 .../Architectures/Transformer/Definition.idr  |   7 +-
 13 files changed, 213 insertions(+), 129 deletions(-)
 create mode 100644 src/Data/Container/Interfaces.idr
 create mode 100644 src/Data/Container/Object/Implementations.idr

diff --git a/pack.toml b/pack.toml
index d241341..ad1888a 100644
--- a/pack.toml
+++ b/pack.toml
@@ -11,4 +11,5 @@ ipkg = "tensortype-examples.ipkg"
 # [custom.all.tensortype-tests]
 # type = "local"
 # path = "tests"
-# ipkg = "tensortype-tests.ipkg"
\ No newline at end of file
+# ipkg = "tensortype-tests.ipkg"
+
diff --git a/src/Data/Container/Applicative/Definition.idr b/src/Data/Container/Applicative/Definition.idr
index 0747d1b..0af7c38 100644
--- a/src/Data/Container/Applicative/Definition.idr
+++ b/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 ->
diff --git a/src/Data/Container/Interfaces.idr b/src/Data/Container/Interfaces.idr
new file mode 100644
index 0000000..9f76809
--- /dev/null
+++ b/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
+
diff --git a/src/Data/Container/Morphism/Definition.idr b/src/Data/Container/Morphism/Definition.idr
index 906df11..92f96e4 100644
--- a/src/Data/Container/Morphism/Definition.idr
+++ b/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))
\ No newline at end of file
+  = !% \x => let (y ** ky) = f x in (y ** (. ky))
diff --git a/src/Data/Container/Object/Implementations.idr b/src/Data/Container/Object/Implementations.idr
new file mode 100644
index 0000000..342fe31
--- /dev/null
+++ b/src/Data/Container/Object/Implementations.idr
@@ -0,0 +1,16 @@
+module Data.Container.Object.Implementations
+
+import Data.Container.Interfaces
+import Data.Container.Object.Definition
+import Data.Container.Object.Instances
+import Data.Fin
+
+export
+TensorMonoid List where
+  tensorN = !% \x => (0 ** absurd)
+  tensorM = !% \x => ?bbb
+
+export
+TensorMonoid (Vect n) where
+  tensorN = !% \x => (() ** const ())
+  tensorM = !% \x => ?bbb2
diff --git a/src/Data/Container/Object/Instances.idr b/src/Data/Container/Object/Instances.idr
index 034c51f..544661e 100644
--- a/src/Data/Container/Object/Instances.idr
+++ b/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`
diff --git a/src/Data/Container/Products.idr b/src/Data/Container/Products.idr
index 489a915..cbfde5f 100644
--- a/src/Data/Container/Products.idr
+++ b/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) ->
diff --git a/src/Data/Tensor/Tensor.idr b/src/Data/Tensor/Tensor.idr
index 835f867..013466f 100644
--- a/src/Data/Tensor/Tensor.idr
+++ b/src/Data/Tensor/Tensor.idr
@@ -1,10 +1,12 @@
 module Data.Tensor.Tensor
 
-import Data.DPair
+import public Data.DPair
 import public Data.Fin.Split
 
 import public Data.Container
-import Data.Container.Object.Instances as Cont
+import public Data.Container.Interfaces
+import public Data.Container.Object.Instances as Cont
+import public Data.Container.Object.Implementations
 
 import public Misc
 
@@ -12,7 +14,7 @@ import public Misc
 
 {-------------------------------------------------------------------------------
 {-------------------------------------------------------------------------------
-This file defines the main construction of this repository `CTensor`, and 
+This file defines the main construction of this repository `CTensor`, and
 provides instances and utilities for working with them.
 `CTensor` is a datatype which is simply a wrapper around the extension of
 a composition of containers.
@@ -27,7 +29,7 @@ Functionality includes:
 * Converting to and from concrete types
 * Various tensor contractions
 * Slicing for cubical tensors
-* Getters 
+* Getters
 * Setters (TODO)
 * Functionality for general reshaping such as views, traversals
 * Concrete reshape for cubical tensors
@@ -45,7 +47,7 @@ record CTensor (shape : List Cont) (a : Type) where
 
 %name CTensor t, t', t''
 
-||| Cubical tensors. Used name 'Tensor' for backwards compatibility with 
+||| Cubical tensors. Used name 'Tensor' for backwards compatibility with
 ||| terminology in the numpy/pytorch ecosystem
 public export
 Tensor : (shape : List Nat) -> Type -> Type
@@ -65,7 +67,7 @@ namespace NestedTensorUtils
   embed a = MkT (toScalar a)
 
   ||| With the added data of the wrapper around (Ext (Tensor shape) a), this
-  ||| effectively states a list version of the following isomorphism 
+  ||| effectively states a list version of the following isomorphism
   ||| Ext c . Ext d = Ext (c . d)
   public export
   fromExtensionComposition : {shape : List Cont} ->
@@ -74,7 +76,7 @@ namespace NestedTensorUtils
   fromExtensionComposition {shape = (_ :: _)} (sh <| contentAt) = MkT $
     let rest = GetT . fromExtensionComposition . contentAt
     in (sh <| shapeExt . rest) <| \(cp ** fsh) => index (rest cp) fsh
-  
+
   public export
   toExtensionComposition : {shape : List Cont} ->
     CTensor shape a -> composeExtensions shape a
@@ -101,7 +103,7 @@ namespace NestedTensorUtils
   public export
   extToVector : Ext c a -> CTensor [c] a
   extToVector e = MkT $ (shapeExt e <| \_ => ()) <| \(cp ** ()) => index e cp
-   
+
   public export
   vectorToExt : CTensor [c] a -> Ext c a
   vectorToExt (MkT t) = shapeExt (shapeExt t) <| \cp => index t (cp ** ())
@@ -112,7 +114,7 @@ namespace NestedTensorUtils
 
   public export
   fromNestedTensor : CTensor [c] (CTensor cs a) -> CTensor (c :: cs) a
-  fromNestedTensor = embedTopExt . vectorToExt 
+  fromNestedTensor = embedTopExt . vectorToExt
 
   public export
   tensorMapFirstAxis : (f : CTensor cs a -> CTensor ds a) ->
@@ -135,7 +137,7 @@ namespace TensorFromConcrete
   concreteTypeTensor [] {allConcrete = []} = concreteType {cont=Scalar}
   concreteTypeTensor (c :: cs) {allConcrete = Cons @{fc}}
     = (concreteType @{fc}) . (concreteTypeTensor cs)
-  
+
   public export
   concreteTypeFunctor : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
@@ -144,29 +146,29 @@ namespace TensorFromConcrete
     = concreteFunctor {cont=Scalar}
   concreteTypeFunctor {shape = (c :: cs)} {allConcrete = Cons @{fc}}
     = Functor.Compose @{concreteFunctor @{fc} } @{concreteTypeFunctor}
-  
+
   public export
   concreteToExtensions : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
     concreteTypeTensor shape a -> composeExtensions shape a
   concreteToExtensions {shape = []} {allConcrete = []} ct = fromConcreteTy ct
-  concreteToExtensions {shape = (_ :: _)} {allConcrete = Cons} ct = 
-    concreteToExtensions <$> fromConcreteTy ct 
-  
+  concreteToExtensions {shape = (_ :: _)} {allConcrete = Cons} ct =
+    concreteToExtensions <$> fromConcreteTy ct
+
   public export
   extensionsToConcreteType : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
     composeExtensions shape a -> concreteTypeTensor shape a
   extensionsToConcreteType {shape = []} {allConcrete = []} ct = toConcreteTy ct
-  extensionsToConcreteType {shape = (_ :: _)} {allConcrete = Cons @{fc}} ct 
+  extensionsToConcreteType {shape = (_ :: _)} {allConcrete = Cons @{fc}} ct
     = (map @{concreteFunctor @{fc}} extensionsToConcreteType) (toConcreteTy ct)
-  
+
   public export
   toTensor : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
     concreteTypeTensor shape a -> CTensor shape a
   toTensor = fromExtensionComposition . concreteToExtensions
-  
+
   public export
   fromTensor : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
@@ -186,7 +188,7 @@ namespace TensorFromConcrete
     (allConcrete : AllConcrete shape) =>
     concreteTypeTensor shape a -> CTensor shape a
   fromConcreteTy = toTensor
-  
+
   public export
   toConcreteTy : {shape : List Cont} ->
     (allConcrete : AllConcrete shape) =>
@@ -194,7 +196,7 @@ namespace TensorFromConcrete
   toConcreteTy = fromTensor
 
   public export prefix 0 >#, #>
-  
+
   ||| Prefix operator for converting from a concrete type to a tensor
   ||| We read it as a map `>` going into the tensor `#`
   public export
@@ -219,20 +221,20 @@ namespace TensorInstances
       (allAppl : AllApplicative shape) =>
       (x : a) -> CTensor shape a
     tensorReplicate {shape = []} = embed
-    tensorReplicate {shape = (_ :: _)} {allAppl = Cons}
+    tensorReplicate {shape = (_ :: _)} {allAppl = (::) _ _ }
       = fromExtensionComposition
       . pure
       . toExtensionComposition
       . tensorReplicate
-  
+
     public export
     liftA2Tensor : {shape : List Cont} ->
       (allAppl : AllApplicative shape) =>
       CTensor shape a -> CTensor shape b -> CTensor shape (a, b)
     liftA2Tensor {allAppl=[]} (MkT t) (MkT t') = embed (index t (), index t' ())
-    liftA2Tensor {allAppl=Cons} t t' = embedTopExt $
+    liftA2Tensor {allAppl=(::) _ _} t t' = embedTopExt $
       uncurry liftA2Tensor <$> liftA2 (extractTopExt t) (extractTopExt t')
-  
+
     public export
     {shape : List Cont} -> (allAppl : AllApplicative shape) =>
     Applicative (CTensor shape) where
@@ -285,7 +287,7 @@ namespace TensorInstances
 
   -- public export
   -- vectInterfacePos : {n : Nat} -> InterfaceOnPositions (Vect n) DecEq
-  -- vectInterfacePos = MkI 
+  -- vectInterfacePos = MkI
 
   namespace NumericInstances
     public export
@@ -322,7 +324,7 @@ namespace TensorInstances
 
 
   namespace AlgebraInstance
-    ||| Unlike all other instantiations of 'AllX', `AllAlgebra` is not 
+    ||| Unlike all other instantiations of 'AllX', `AllAlgebra` is not
     ||| stating that each container in an list has an algebra, but rather
     ||| 'cumulatively'. For instance, `AllAlgebra [c, d] a` is not defined as
     ||| `Algebra c a` and `Algebra d a`, bur rather as `Algebra c (Algebra d a)`
@@ -469,7 +471,7 @@ namespace TensorInstances
       Applicative f =>
       (a -> f b) -> CTensor shape a -> f (CTensor shape b)
     tensorTraverse {allTraversable = []} f t = pure <$> f (extract t)
-    tensorTraverse {allTraversable = Cons} f t = embedTopExt <$> 
+    tensorTraverse {allTraversable = Cons} f t = embedTopExt <$>
       traverse (\ct => tensorTraverse f ct) (extractTopExt t)
 
     public export
@@ -532,7 +534,7 @@ namespace TensorInstances
     --   lookup = ?eee
     --   tabulate = ?eeee
 
-    public export 
+    public export
     transposeMatrix : {i, j : Cont} ->
       (allNaperian : AllNaperian [i, j]) =>
       CTensor [i, j] a -> CTensor [j, i] a
@@ -541,11 +543,11 @@ namespace TensorInstances
       . transpose
       . toExtensionComposition
 
-    
+
     tm : Tensor [2, 3] a -> Tensor [3, 2] a
     tm t = transposeMatrix t
 
-    tmp : {i, j : Nat} -> Tensor [i, j] a -> Tensor [j, i] a 
+    tmp : {i, j : Nat} -> Tensor [i, j] a -> Tensor [j, i] a
     tmp t = transposeMatrix t
 
     ttm : {i, j : Cont} -> AllNaperian [i, j] => CTensor [i, j] a -> CTensor [j, i] a
@@ -562,7 +564,7 @@ namespace TensorInstances
     public export
     data AllShow : List Cont -> Type -> Type where
       Nil : Show a => AllShow [] a
-      -- for type below, we should be able to define what shExt is without referencing CTensor cs a? 
+      -- for type below, we should be able to define what shExt is without referencing CTensor cs a?
       Cons : Show (c `fullOf` CTensor cs a) =>
        AllShow (c :: cs) a
 
@@ -612,23 +614,26 @@ namespace TensorInstances
       Algebra (CTensor shape) a => AllApplicative shape =>
       CTensor shape a -> CTensor shape a -> CTensor [] a
     dot xs ys = dotWith (*) xs ys
-    
+
     public export
-    outerWith : {i, j : Cont} -> (allAppl : AllApplicative [i, j]) =>
+    outerWith : {i, j : Cont} ->
+      (TensorMonoid i) =>
+      (TensorMonoid j) =>
       (a -> b -> c) ->
       CTensor [i] a -> CTensor [j] b -> CTensor [i, j] c
-    outerWith {allAppl = Cons} f t t' =
+    outerWith f t t' =
       let tt = (\(t, a) => strength a t) <$> strength t' t
       in uncurry f <$> fromNestedTensor tt
 
     public export
-    outer : {i, j : Cont} -> Num a => 
-      (allAppl : AllApplicative [i, j]) =>
+    outer : {i, j : Cont} -> Num a =>
+      (TensorMonoid i) =>
+      (TensorMonoid j) =>
       CTensor [i] a -> CTensor [j] a -> CTensor [i, j] a
     outer = outerWith (*)
 
     public export
-    matrixVectorProduct : Num a => {f, g : Cont} -> AllApplicative [g] =>
+    matrixVectorProduct : Num a => {f, g : Cont} -> TensorMonoid g =>
       AllAlgebra [g] a =>
       CTensor [f, g] a -> CTensor [g] a -> CTensor [f] a
     matrixVectorProduct m v = fromNestedTensor $
@@ -637,10 +642,10 @@ namespace TensorInstances
 
     public export
     vectorMatrixProduct : Num a => {f, g : Cont} ->
-      (allAppl : AllApplicative [f]) =>
+      (TensorMonoid f) =>
       Algebra (Ext f) (CTensor [g] a) =>
       CTensor [f] a -> CTensor [f, g] a -> CTensor [g] a
-    vectorMatrixProduct {allAppl = Cons} v m =
+    vectorMatrixProduct v m =
       let em : Ext f (CTensor [g] a) := extractTopExt m
           ev : Ext f (CTensor [] a) := extractTopExt v
       in reduce $ (\(x, gx) => ((extract x) *) <$> gx) <$> liftA2 ev em
@@ -648,19 +653,19 @@ namespace TensorInstances
       --in extract $ dotWith (\x, gx => (x *) <$> gx) v t
 
     public export
-    matMul : Num a => {f, g, h : Cont} -> AllApplicative [g] =>
+    matMul : Num a => {f, g, h : Cont} -> TensorMonoid g =>
       Algebra (Ext g) (CTensor [h] a) =>
       CTensor [f, g] a -> CTensor [g, h] a -> CTensor [f, h] a
-    matMul m1 m2 = fromNestedTensor $ 
+    matMul m1 m2 = fromNestedTensor $
       toNestedTensor m1 <&> (\row => vectorMatrixProduct row m2)
 
     -- "ij,kj->ki"
     public export
     matrixMatrixProduct : {f, g, h : Cont} -> Num a =>
-      AllApplicative [g] =>
+      TensorMonoid g =>
       AllAlgebra [g] a =>
       CTensor [f, g] a -> CTensor [h, g] a -> CTensor [h, f] a
-    matrixMatrixProduct m1 m2 = fromNestedTensor $ 
+    matrixMatrixProduct m1 m2 = fromNestedTensor $
       matrixVectorProduct m1 <$> toNestedTensor m2
 
 tt0 : CTensor [] Integer
@@ -774,7 +779,7 @@ namespace SetterGetter
       (p : c.Pos (shapeExt (extractTopExt t))) ->
       Index cs (index (extractTopExt t) p) ->
       Index (c :: cs) t
-  
+
   %name Index is, js
 
   public export
@@ -790,7 +795,7 @@ namespace SetterGetter
     (t : CTensor shape a) -> Index shape t -> a
   (@@) = index
 
-  public export 
+  public export
   set : {shape : List Cont} ->
     (t : CTensor shape a) ->
     (iop : InterfaceOnPositions (Tensor shape) Eq) =>
@@ -811,11 +816,11 @@ namespace SetterGetter
   public export
   t00 : CTensor [Maybe, List] Integer
   t00 = ># Just [10, 20, 30, 40, 50, 60, 70]
-  
+
   public export
   t11 : Tensor [2, 3] Integer
   t11 = ># [[1,2,3], [4,5,6]]
-  
+
   public export
   t22 : CTensor [BinTree, List] Integer
   t22 = ># Node [1,2] (Leaf [3,4]) (Leaf [5,6])
@@ -825,7 +830,7 @@ namespace SetterGetter
 
   t333 : CTensor [Vect 2] Integer
   t333 = ># [1, 2]
-  
+
   t44 : CTensor [] Integer
   t44 = ># 13
 
@@ -838,11 +843,11 @@ namespace CubicalSetterGetter
   data IndexC : List Nat -> Type where
     Nil : IndexC []
     (::) : Fin n -> IndexC ns -> IndexC (n :: ns)
-  
+
   public export
   indexC : {shape : List Nat} -> Tensor shape a -> IndexC shape -> a
   indexC t [] = index (GetT t) ()
-  indexC t (i :: is) = indexC (index (GetT $ toNestedTensor t) (i ** ())) is 
+  indexC t (i :: is) = indexC (index (GetT $ toNestedTensor t) (i ** ())) is
 
   public export
   setC : {shape : List Nat} ->
@@ -893,4 +898,4 @@ namespace Concatenate
   public export
   concat : {x : Nat} ->
     Tensor (x :: shape) a -> Tensor (y :: shape) a -> Tensor (x + y :: shape) a
-  concat t t' = embedTopExt $ extractTopExt t ++ extractTopExt t'
\ No newline at end of file
+  concat t t' = embedTopExt $ extractTopExt t ++ extractTopExt t'
diff --git a/src/Data/Tensor/Utils.idr b/src/Data/Tensor/Utils.idr
index f139972..6965915 100644
--- a/src/Data/Tensor/Utils.idr
+++ b/src/Data/Tensor/Utils.idr
@@ -5,6 +5,7 @@ import System.Random
 
 import Data.Tensor.Tensor
 import Data.Container.SubTerm
+import Data.Container.Object.Implementations
 import Misc
 
 
@@ -33,7 +34,7 @@ namespace CommonNames
   public export
   CVector : (c : Cont) -> (dtype : Type) -> Type
   CVector c dtype = CTensor [c] dtype
-  
+
   public export
   CMatrix : (row, col : Cont) -> (dtype : Type) -> Type
   CMatrix row col dtype = CTensor [row, col] dtype
@@ -45,19 +46,19 @@ namespace CommonNames
   public export
   Vector : (n : Nat) -> (dtype : Type) -> Type
   Vector n dtype = Tensor [n] dtype
-  
+
   public export
   Matrix : (row, col : Nat) -> (dtype : Type) -> Type
   Matrix row col dtype = Tensor [row, col] dtype
 
 namespace ZerosOnes
   public export
-  zeros : Num a => {shape : List Cont} -> AllApplicative shape => 
+  zeros : Num a => {shape : List Cont} -> AllApplicative shape =>
     CTensor shape a
   zeros = tensorReplicate (fromInteger 0)
-  
+
   public export
-  ones : Num a => {shape : List Cont} -> AllApplicative shape => 
+  ones : Num a => {shape : List Cont} -> AllApplicative shape =>
     CTensor shape a
   ones = tensorReplicate (fromInteger 1)
 
@@ -74,7 +75,7 @@ namespace ZerosOnes
   identity = fromBool <$> identityBool
 
 namespace Range
-  {----- 
+  {-----
   This one is interesting, as in the cubical case it's effectively a version of 'tabulate' from Naperian functors.
   The cubical version is implemented first, and it's possible that a more general version of rangeA can be defined for container based tensors, possibly by tabulating contents of each shape respectively
   -----}
@@ -107,14 +108,14 @@ namespace Flip
   flip : (axis : Fin (length shape)) -> Tensor shape a -> Tensor shape a
 
 namespace Size
-  {----- 
+  {-----
   Can we measure the size of a tensor of containers?
   Likely need to impose an additional constraint that the set of positions is enumerable
   -----}
   ||| Number of elements in a non-cubical tensor
   public export
   cSize : {shape : List Cont} -> CTensor shape a -> Nat
-  
+
   ||| Number of elements in a cubical tensor
   public export
   size : {shape : List Nat} -> (0 _ : Tensor shape a) -> Nat
@@ -127,7 +128,7 @@ namespace Flatten
   public export
   cFlatten : Foldable (CTensor shape) => CTensor shape a -> List a
   cFlatten = toList
-  
+
   ||| Flatten a cubical tensor into a vector
   ||| Number of elements is known at compile time
   ||| Can even be zero, if any of shape elements is zero
@@ -146,7 +147,7 @@ namespace Max
   max : Foldable (CTensor shape) => Ord a =>
     CTensor shape a -> Maybe a
   max = maxInList . cFlatten
-  
+
   -- TODO Fix for strided
   -- max {shape = []} t = maxA (FromCubicalTensor t)
   -- max {shape = (s :: ss)} t = let tt = maxA (FromCubicalTensor t) in ?max_rhs_1
@@ -159,14 +160,14 @@ namespace OneHot
   public export
   oneHot : Num a => {n : Nat} ->
     (i : Fin n) -> Tensor [n] a
-  oneHot i = set (zeros {shape=[Vect n]}) [i] 1 
+  oneHot i = set (zeros {shape=[Vect n]}) [i] 1
 
 
 namespace Triangular
   public export
   cTriBool : {c : Cont} ->
     (ip : InterfaceOnPositions c MOrd) =>
-    AllApplicative [c] =>
+    TensorMonoid c =>
     (sh : c.Shp) -> CTensor [c, c] Bool
   cTriBool {ip = MkI {p}} sh
     = let cPositions = positions {sh=sh}
@@ -223,7 +224,7 @@ namespace Misc
   public export
   mean : {shape : List Nat} ->
     Cast Nat a =>
-    Fractional a => 
+    Fractional a =>
     Algebra (Tensor shape) a =>
     Tensor shape a -> a
   mean t = reduce t / cast (size t)
@@ -237,6 +238,7 @@ namespace Misc
 
 
 
+
 namespace Traversals
   public export
   inorder : CTensor [BinTreeNode] a -> CTensor [List] a
@@ -249,15 +251,15 @@ namespace Random
   Traversable (Tensor shape) =>
   Random (Tensor shape a) where
     randomIO = sequence (pure randomIO)
-   
-    randomRIO (lo, hi) = sequence $ randomRIO <$> liftA2 lo hi 
 
--- Idris can't find the parametric randomIO interface so reimpementing here 
+    randomRIO (lo, hi) = sequence $ randomRIO <$> liftA2 lo hi
+
+-- Idris can't find the parametric randomIO interface so reimpementing here
 public export
 random : Num a => Random a => HasIO io =>
   (shape : List Nat) ->
-  Applicative (Tensor shape) => 
-  Traversable (Tensor shape) => 
+  Applicative (Tensor shape) =>
+  Traversable (Tensor shape) =>
   io (Tensor shape a)
 random shape = sequence $ pure $ randomRIO (0, 1)
 
@@ -271,7 +273,7 @@ tttt : Traversable (Tensor [2])
 tttt = %search
 
 testRand : IO (Tensor [2, 3] Double)
-testRand = do 
+testRand = do
   t <- random [2,3]
   printLn $ show t
   pure t
diff --git a/src/NN/Architectures/Affine.idr b/src/NN/Architectures/Affine.idr
index fc8feca..3ac51ea 100644
--- a/src/NN/Architectures/Affine.idr
+++ b/src/NN/Architectures/Affine.idr
@@ -14,16 +14,18 @@ record AffineLayerParams (x, y : Cont) (a : Type) where
 public export
 affineImpl : {x, y : Cont} -> Num a =>
   AllAlgebra [x] a =>
-  (allAppl : AllApplicative [x, y]) =>
+  TensorMonoid x =>
+  TensorMonoid y =>
   CTensor [x] a -> AffineLayerParams x y a -> CTensor [y] a
-affineImpl {allAppl = Cons} input (MkParams weights bias)
+affineImpl input (MkParams weights bias)
   = matrixVectorProduct weights input + bias
 
 public export
 affinePara : {x, y : Cont} -> {a : Type} -> Num a =>
   AllAlgebra [x] a =>
-  AllApplicative [x, y] =>
+  TensorMonoid x =>
+  TensorMonoid y =>
   CTensor [x] a -\-> CTensor [y] a
 affinePara = MkPara
   (const (AffineLayerParams x y a))
-  affineImpl
\ No newline at end of file
+  affineImpl
diff --git a/src/NN/Architectures/MLP.idr b/src/NN/Architectures/MLP.idr
index 1ed74ed..5fbb439 100644
--- a/src/NN/Architectures/MLP.idr
+++ b/src/NN/Architectures/MLP.idr
@@ -12,7 +12,7 @@ public export
 multiLayerPerceptron : {a : Type} -> Num a =>
   {ieva : Cont} ->
   (allAlg : AllAlgebra [ieva] a) =>
-  (allAppl : AllApplicative [ieva]) =>
+  (allAppl : TensorMonoid ieva) =>
   (numLayers : Nat) ->
   (activation : CTensor [ieva] a -\-> CTensor [ieva] a) ->
   {default False lastLayerActivation : Bool} ->
@@ -24,6 +24,7 @@ multiLayerPerceptron 1 activation {lastLayerActivation = True}
   = composePara affinePara activation
 multiLayerPerceptron (S (S k)) activation
   = composePara (composePara affinePara activation) (multiLayerPerceptron (S k) activation {lastLayerActivation = lastLayerActivation})
+  {-
 
 public export
 mlpNonDependentPara : {a : Type} -> Num a =>
@@ -34,7 +35,7 @@ mlpNonDependentPara : {a : Type} -> Num a =>
   (activation : CTensor [ieva] a -> CTensor [ieva] a) ->
   {default False lastLayerActivation : Bool} ->
   IsNotDependent (multiLayerPerceptron numLayers (trivialParam activation) {lastLayerActivation = lastLayerActivation})
-mlpNonDependentPara 0 activation = MkNonDep () (\t, _ => t)
+mlpNonDependentPara 0 activation = ?oqwi -- MkNonDep () (\t, _ => t)
 mlpNonDependentPara 1 activation {lastLayerActivation = False}
   = MkNonDep (AffineLayerParams ieva ieva a)
     (\x, p => (Run (multiLayerPerceptron 1 (trivialParam activation) {lastLayerActivation = False})) x p)
@@ -64,10 +65,10 @@ exampleBias : Tensor [2] Double
 exampleBias = ># [0, 0]
 
 public export
-layerParam : AffineLayerParams (Vect 2) (Vect 2) Double 
+layerParam : AffineLayerParams (Vect 2) (Vect 2) Double
 layerParam = MkParams exampleParam exampleBias
 
 public export
 exampleOutput : Tensor [2] Double
 exampleOutput = Run (simpleNLayerNet 2) exampleInput
-  ((layerParam ** ()) ** layerParam) 
\ No newline at end of file
+  ((layerParam ** ()) ** layerParam)
diff --git a/src/NN/Architectures/Transformer/Attention.idr b/src/NN/Architectures/Transformer/Attention.idr
index 73b1e53..38f51b6 100644
--- a/src/NN/Architectures/Transformer/Attention.idr
+++ b/src/NN/Architectures/Transformer/Attention.idr
@@ -2,20 +2,22 @@ module NN.Architectures.Transformer.Attention
 
 import Data.Tensor
 import Data.Para
+import Data.Container.Interfaces
 import NN.Architectures.Softargmax
 
 ||| Generalised form of attention
 public export
 crossAttention : {a : Type} -> Num a =>
   {inputStructure, crossStructure, features : Cont} ->
-  (allAppl : AllApplicative [inputStructure, features]) =>
+  (TensorMonoid features) =>
+  (TensorMonoid inputStructure) =>
   (allAlg : AllAlgebra [inputStructure, features] a) =>
   {default id causalMask : CTensor [crossStructure, inputStructure] a -> CTensor [crossStructure, inputStructure] a} ->
   (softargmax : CTensor [inputStructure] a -> CTensor [inputStructure] a) ->
   (q, v : CTensor [inputStructure, features] a) ->
   (k : CTensor [crossStructure, features] a) ->
   CTensor [crossStructure, features] a
-crossAttention {allAlg=Cons} {allAppl=Cons} {causalMask} softargmax q v k =
+crossAttention {allAlg=Cons} {causalMask} softargmax q v k =
   let attentionMatrix : CTensor [crossStructure, inputStructure] a
       attentionMatrix = (q `matrixMatrixProduct` k)
   in (softargmax <-$> (causalMask attentionMatrix)) `matMul` v
@@ -24,14 +26,15 @@ crossAttention {allAlg=Cons} {allAppl=Cons} {causalMask} softargmax q v k =
 public export
 selfAttention : {a : Type} -> Num a =>
   {inputStructure, features : Cont} ->
-  (allAppl : AllApplicative [inputStructure, features]) =>
+  (TensorMonoid inputStructure) =>
+  (TensorMonoid features) =>
   (allAlg : AllAlgebra [inputStructure, features] a) =>
   {default id causalMask : CTensor [inputStructure, inputStructure] a -> CTensor [inputStructure, inputStructure] a} ->
   (softargmax : CTensor [inputStructure] a -> CTensor [inputStructure] a) ->
   (q, v, k : CTensor [inputStructure, features] a) ->
   CTensor [inputStructure, features] a
 selfAttention {causalMask} = crossAttention {causalMask}
-  
+
 ||| Data structure for holding parameters of self-attention
 public export
 record CSelfAttentionParams (features : Cont) (a : Type) where
@@ -44,14 +47,15 @@ record CSelfAttentionParams (features : Cont) (a : Type) where
 public export
 SAImpl : {a : Type} -> Num a =>
   {inputStructure, features : Cont} ->
-  (allAppl : AllApplicative [inputStructure, features]) =>
+  (TensorMonoid inputStructure) =>
+  (TensorMonoid features) =>
   (allAlg : AllAlgebra [inputStructure, features] a) =>
   {default id causalMask : CTensor [inputStructure, inputStructure] a -> CTensor [inputStructure, inputStructure] a} ->
   (softargmax : CTensor [inputStructure] a -> CTensor [inputStructure] a) ->
   (input : CTensor [inputStructure, features] a) ->
   (params : CSelfAttentionParams features a) ->
   CTensor [inputStructure, features] a
-SAImpl {allAppl = Cons} {allAlg = Cons} {causalMask} softargmax input (MkCSAParams queryMat valueMat keyMat)
+SAImpl {allAlg = Cons} {causalMask} softargmax input (MkCSAParams queryMat valueMat keyMat)
   = let queries = queryMat `matrixMatrixProduct` input
         keys = keyMat `matrixMatrixProduct` input
         values = valueMat `matrixMatrixProduct` input
@@ -61,7 +65,8 @@ SAImpl {allAppl = Cons} {allAlg = Cons} {causalMask} softargmax input (MkCSAPara
 public export
 SelfAttention : {a : Type} -> Num a =>
   {inputStructure, features : Cont} ->
-  (allAppl : AllApplicative [inputStructure, features]) =>
+  (TensorMonoid inputStructure) =>
+  (TensorMonoid features) =>
   (allAlg : AllAlgebra [inputStructure, features] a) =>
   {default id causalMask : CTensor [inputStructure, inputStructure] a -> CTensor [inputStructure, inputStructure] a} ->
   (softargmax : CTensor [inputStructure] a -> CTensor [inputStructure] a) ->
@@ -78,9 +83,9 @@ public export
 causalMask : {a : Type} -> Num a =>
   {c : Cont} -> Exp a =>
   InterfaceOnPositions c MOrd =>
-  AllApplicative [c] =>
+  TensorMonoid c =>
   CTensor [c, c] a -> CTensor [c, c] a
-causalMask attentionMatrix = 
+causalMask attentionMatrix =
   let contShape : c.Shp
       contShape = shapeExt (shapeExt (GetT attentionMatrix))
-  in maskedFill attentionMatrix (not <$> cTriBool contShape) minusInfinity
\ No newline at end of file
+  in maskedFill attentionMatrix (not <$> cTriBool contShape) minusInfinity
diff --git a/src/NN/Architectures/Transformer/Definition.idr b/src/NN/Architectures/Transformer/Definition.idr
index ddc7c96..a9171b2 100644
--- a/src/NN/Architectures/Transformer/Definition.idr
+++ b/src/NN/Architectures/Transformer/Definition.idr
@@ -15,13 +15,14 @@ import NN.Architectures.Utils
 public export
 Transformer : {a : Type} -> Num a => Ord a =>
   {inputStructure, features : Cont} ->
-  (allAppl : AllApplicative [inputStructure, features]) =>
+  (TensorMonoid inputStructure) =>
+  (TensorMonoid features) =>
   (allAlg : AllAlgebra [inputStructure, features] a) =>
   {default id causalMask : CTensor [inputStructure, inputStructure] a -> CTensor [inputStructure, inputStructure] a} ->
   (softargmax : CTensor [inputStructure] a -> CTensor [inputStructure] a) ->
   CTensor [inputStructure, features] a -\-> CTensor [inputStructure, features] a
-Transformer {allAppl = Cons} {allAlg = Cons} softargmax
+Transformer {allAlg = Cons} softargmax
   = composePara (addResidual (SelfAttention softargmax)) (addResidual ffnet)
     where
       ffnet : CTensor [inputStructure, features] a -\-> CTensor [inputStructure, features] a
-      ffnet = paraMapFirstAxis (multiLayerPerceptron {a=a} {ieva=features} 2 (trivialParam relu) {lastLayerActivation=False}) 
\ No newline at end of file
+      ffnet = paraMapFirstAxis (multiLayerPerceptron {a=a} {ieva=features} 2 (trivialParam relu) {lastLayerActivation=False})

From 2022631de459d2024eed9e51715a9a07ce30b9d9 Mon Sep 17 00:00:00 2001
From: Andre Videla <me@andrevidela.com>
Date: Wed, 14 Jan 2026 11:07:13 +0000
Subject: [PATCH 2/2] add missing implementation for monoid instance

---
 src/Data/Container/Object/Implementations.idr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/Container/Object/Implementations.idr b/src/Data/Container/Object/Implementations.idr
index 342fe31..3e14fe2 100644
--- a/src/Data/Container/Object/Implementations.idr
+++ b/src/Data/Container/Object/Implementations.idr
@@ -4,13 +4,14 @@ 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 = !% \x => ?bbb
+  tensorM = !% \(x1, x2) => (x1 * x2 ** splitProd)
 
 export
 TensorMonoid (Vect n) where
   tensorN = !% \x => (() ** const ())
-  tensorM = !% \x => ?bbb2
+  tensorM = !% \x => (() ** (\x => (x, x)))