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