[Haskell-cafe] Size-indexed monoids

[Kosyrev Serge]

Good day!

What is the proper type class for stronger-typed (size-indexed) monoids:
  - that is, monoids carrying their "size" in the type
  - preferably as GHC.TypeLits.Nat
  - preferably on Hackage
?

I'm quite prepared to the idea that a monoid is an entirely wrong abstraction,
from a category-theoretic standpoint, so I would gladly learn of a better one : -)

Use case:

> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, UnicodeSyntax, StandaloneDeriving #-}
>
> module Understanding.Types where
>
> import GHC.TypeLits
>
> data T (depth ∷ Nat) p where
>   TZ ∷ T 0 p
>   TS ∷ (Show p, CmpNat (m + 1) n ~ EQ) ⇒
>     { payload ∷ p
>     , next    ∷ T m a } → T n a
> deriving instance Show p ⇒ Show (T d p)
>
> instance Monoid (T d p) where
>   mempty    = TZ
>   mappend     TZ         TZ      = TZ
>   mappend     TZ      t@(TS _ _) = t
>   mappend  t@(TS _ _)    TZ      = t
>   mappend tl@(TS pl nl)  tr      = TS pl $ mappend nl tr

As it is, even the mempty case rejects such a blatant violation of
polymorphism, since `T 0 p` cannot unify with `T n p`.

So, ideally (I think), I would like something like this:

> class TypedMonoid a where
>   tmempty  ∷ a 0
>   tmappend ∷ a n → a m → a (n + m)

--
с уважениeм / respectfully,
Косырев Сергей
--
“Most deadly errors arise from obsolete assumptions.”
  -- Frank Herbert, Children of Dune