Never even compiled, but this is how I'd think of Maxels.

Maxel.hs

module Maxel where

import Control.Monad
import Data.Discrimination.Grouping
import Data.Map as Map
import Data.Tuple (swap)

-- M a b is a generalization of a b-valued multiset and a maxel
-- M (Fin n) b acts as an MSet(n)
-- M (x,y) b acts as a 'traditional' maxel
-- M (x,y,z) b acts more like a tensor, mul can be used to 
-- select out a set of dimensions to trace and to merge indices
-- this gives a tensor-like maxel (a 'tensel'?) 
-- or 'holor'-like maxel (a 'holel'?)

newtype M a r = M [(a,r)]
  deriving Show

-- injective mappings desired
mapxel' :: (a -> b) -> M a r -> M b r
mapxel' f (M xs) = M (first f xs)

-- mapxel :: (Grouping b, Realm r) => (a -> b) -> M a r -> M b r
-- mapxel f (M xs) = M $ _ -- TODO

transpose :: M (x,y) b -> M (y,x) b
transpose = mapxel' swap

-- compute the direct product of multisets
dprod :: M a r -> M b r -> M (a, b) r
dprod (M xs) (M ys) = M [ ((x,y),s∙t) | (x,s) <- xs, (y,t) <- ys ]

instance (Grouping a, Realm r, PartialOrder r) => Eq (M a r) where
  x == y = x ⊆ y && y ⊆ x

-- lift a pairwise symmetric operation
pairwise :: Grouping a => (b -> b -> b) -> M a b -> M a b -> M a b
pairwise f (M xs) (M ys) = xs ++ ys
  & map duplicate 
  & runGroup grouping
  & M . map (fst . head &&& foldr1 f . fmap snd)

type MSet a = M a Natural
type IntMset a = M a Integer

class Join m where (∨) :: m -> m -> m
instance Join Void where (∨) = absurd
instance Join () where (∨) = mempty
instance Join Bool where (∨) = (||)
instance Join Natural where (∨) = max
instance Join Integer where (∨) = max
instance (Join a, Join b) => Join (a, b) where (a,b) ∨ (c,d) = (a ∨ c, b ∨ d)
instance Join a => Join (b -> a) where f ∨ g = \x -> f x ∨ g x
instance (Grouping a, Join b) => Join (M a b) where (∨) = pairwise (∨)

class Join m => Bottom m where bottom :: m
instance Bottom () where bottom = ()
instance Bottom Bool where bottom = False
instance Bottom Natural where bottom = 0
instance Bottom a => Bottom (b -> a) where bottom = const bottom
instance (Bottom a, Bottom b) => Bottom (a, b) where bottom = (bottom,bottom)
 
class Meet m where (∨) :: m -> m -> m
instance Meet Bool where (∧) = (&&)
instance Meet Natural where (∧) = min
instance Meet Integer where (∧) = min
instance (Meet a, Meet b) => Meet (a,b) where (a,b)∧(c,d)=(a∧c,b∧d)
instance Meet a => Meet (b -> a) where f ∧ g = \x -> f x ∧ g x
instance (Grouping a, Meet b) => Meet (M a b) where (∧) = pairwise (∧)

class Meet m => Top m where top :: m
instance Top () where top = ()
instance Top Bool where top = True
instance Top a => Top (b -> a) where top = const top
instance (Top a, Top b) => Top (a,b) where top = (top,top)

-- this is merely a distinguished element, it is not necessarily the
-- top or bottom of any lattice
class Zero m where zero :: m
instance Zero () where zero = ()
instance Zero Natural where zero = 0
instance Zero Integer where zero = 0
--instance Ord a => Zero (Multi a b) where zero = Multi mempty
instance Zero a => Zero (b -> a) where zero = const zero
instance (Zero a, Zero b) => Zero (a,b) where zero = (zero,zero)
instance Zero (M a b) where zero = M []

class Zero m => IsZero m where isZero :: m -> Bool
instance IsZero Natural where isZero = (==0)
instance IsZero Integer where isZero = (==0)
instance Ord a => IsZero (Multi a b) where isZero (Multi m) = null m
instance (IsZero a, IsZero b) => IsZero (a,b) where isZero (a,b) = isZero a && isZero b
-- instance (Realm b, IsZero b) => IsZero (M a b) where isZero = 

-- m ∨ (m ∧ n) = m
-- m ∧ (m ∨ n) = m
class (Meet m, Join m) => Lattice m where
instance Lattice Natural
instance Lattice Integer
instance (Ord a, Lattice b) => DistributiveLattice (Multi a b) 
instance (Lattice a, Lattice b) => Lattice (a, b)
instance (Grouping a, Lattice b) => Lattice (M a b)

-- | k ∧ (m ∨ n) = (k ∧ m) ∨ (k ∧ n)
class Lattice m => DistributiveLattice m
instance DistributiveLattice Natural
instance DistributiveLattice Integer
--instance (Ord a, DistributiveLattice b) => DistributiveLattice (Multi a b) 
instance (DistributiveLattice a, DistributiveLattice b) => DistributiveLattice (a, b)
instance (Grouping a, DistributiveLattice b) => DistributiveLattice (M a b)

class (Zero m, DistributiveLattice m) => Realm m where
  -- | associative, commutative, with unit zero
  -- @
  -- k ⊕ (m ∨ n) = (k ⊕ m) ∨ (k ⊕ n)
  -- k ⊕ (m ∧ n) = (k ⊕ m) ∧ (k ⊕ n)
  -- zero ⊕ m = m = m ⊕ zero
  -- @
  -- Cancellation: k + n = m + n ==> k = m
  -- Summation: (m ∨ n) ⊕ (m ∧ n) = m ⊕ n
  (⊕):: m -> m -> m

  -- m ⊖ n = m - (m ∧ n), saturating subtraction
  -- (k + m) ∧ n = (k ∧ n) + m ∧ (n ⊖ k)
  (⊖) :: m -> m -> m
  default (⊖) :: (Ord m, Num m) => m -> m -> m
  m ⊖ n | m >= n = m - n
        | otherwise = zero

  -- k∘(m + n) = k∘m + k∘n
  -- (k+l)∘m = k∘m + l∘m
  -- (k*l)∘m = k∘(l∘m)
  -- 1∘m = m
  -- 0∘m = zero
  (∘) :: Natural -> m -> m
  n ∘ m = getAdd $ mtimes n $ Add m

  -- assertion: every realm has a multiplication
  (∙) :: m -> m -> m


instance (Realm a, Realm b) => Realm (a, b) where
  (a,b)⊕(c,d) = (a⊕c,b⊕d)
  (a,b)⊖(c,d) = (a⊖c,b⊖d)
  n∘(a,b) = (n∘a,n∘b)
  (a,b)∙(c,d) = (a∙c,b∙d)
  

instance Realm Integer where
  (⊕) = (+)
  n ∘ i = fromIntegral n * i
  (∙) = (*)
  
instance Realm Natural where
  (⊕) = (+)
  (∘) = (*)
  (∙) = (*)

instance (Grouping a, Realm b, DistinguishedZero b) => Realm (M a b) where
  n∘M xs = M (fmap (n∘) <$> xs)
  (⊕) = pairwise (⊕)
  M as ⊖ M bs = M $ joining grouping go fst fst as bs where
    go :: [(a,b)] -> [(a,b)] -> (a,b)
    go xs ys = (fst $ head xs, add snd xs ⊖ add snd ys)
  (∙) = mul dup dup fst (∙)

-- tensor multiplication
mul
  :: (Grouping j, Realm c)
  => (x -> (i,j))
  -> (y -> (j,k))
  -> ((i,k) -> z)
  -> (a -> b -> c)
  -> M x a -> M y b -> M z c
mul f g h i (M xas) (M ybs) = M $ joining grouping go (snd.f) (fst.g) xas ybs where
  go :: [(x,a)] -> [(y,b)] -> [(z,c)]
  go xs ys =
    ( h (fst $ f $ head xs) (snd $ g $ head ys)
    , add snd xs ∙ add snd ys
    )

(^*^) :: (Grouping b, Realm r) => M (a,b) r -> M (b,c) r -> M (a,c) r
(^*^) = mul id id id (∙)
 
newtype Add a = Add { getAdd :: a }
instance Realm a => Semigroup (Add a) where Add a <> Add b = Add (a ⊕ b)
instance Realm a => Monoid (Add a) where mempty = Add zero

add :: (Foldable f, Realm b) => (a -> b) -> f a -> b
add f = getAdd . foldMap (Add . f) 

size :: (Foldable f, Realm b) => f b -> b
size = getAdd . foldMap Add

class Realm => IntegralRealm m where
  neg :: m -> m 
  neg = minus zero
  minus :: m -> m -> m
  minus m n = m ⊕ neg n
  {-# minimal neg | minus #-}

instance IntegralRealm Integer where
  neg = negate
  minus = (-) 

instance IntegralRealm b => IntegralRealm (M a b) where
  neg (Multi m) = Multi (fmap (fmap neg) m)
  minus m n = m ⊕ neg n

class PartialOrder m where
  (⊆) :: m -> m -> Bool
  default (⊆) :: Ord m => m -> m -> Bool
  (⊆) = (<=) 

instance PartialOrder Void
instance PartialOrder ()
instance PartialOrder Bool
instance PartialOrder Natural
instance PartialOrder Integer
instance (PartialOrder a, PartialOrder b) =>  PartialOrder (a,b) where
  (a,b) ⊆ (c,d) = a⊆c && b⊆d

instance (Grouping a, Realm b, PartialOrder b) => PartialOrder (M a b) where
  M as ⊆ M bs
    = all (spanEither $ (⊆) `on` size)
    $ disc grouping
    $ fmap Left as ++ fmap Right bs