[Haskell-cafe] Size-indexed monoids

[Ertugrul Söylemez]

> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170222/24bd748b/attachment.sig>