Re: [Haskell-cafe] Size-indexed monoids

22 Feb 2017

      ...
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 don't think monoid is the correct term simply because it's indexed.
I've called them measured monoids, and the following approach seems to
work well:

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeInType #-}

    import GHC.Types (Type)

    class TMonoid a where
        type family Empty a :: a
        type family Append a (x :: a) (y :: a) :: a

    data Nat = Z | S Nat

    instance TMonoid Nat where
        type Empty Nat = Z
        type Append Nat Z y = y
        type Append Nat (S x) y = S (Append Nat x y)

    class MeasuredMonoid (a :: n -> Type) where
        mmEmpty  :: a (Empty n)
        mmAppend :: a n1 -> a n2 -> a (Append n n1 n2)

    data Vec :: Type -> Nat -> Type where
        Nil  :: Vec a Z
        Cons :: a -> Vec a n -> Vec a (S n)

    instance MeasuredMonoid (Vec a) where
        mmEmpty = Nil
        mmAppend Nil ys = ys
        mmAppend (Cons x xs) ys = Cons x (mmAppend xs ys)

I couldn't tell you whether there is a library for that though.

Re: [Haskell-cafe] Size-indexed monoids

Ertugrul Söylemez