[Haskell-cafe] Size-indexed monoids

[Sergey Kosyrev]

Adam, 

Somewhat earlier, Adam Gundry wrote:
> You might take a look at the rather lovely ghc-typelits-natnormalise
> plugin. I haven't tried, but assuming you adjust the code to use a type
> equality constraint rather than CmpNat, I think it should automatically
> solve the problematic constraint.

The use of ghc-typelits-natnormalise turned out to be a huge success!
(modulo the typical z-versus-s issue, that caused some guessing : -)

I only made the package available to Cabal, added the one-liner pragma,
made the trivial modification you suggested, and the following just worked:

> {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
> {-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving, TypeOperators, UnicodeSyntax #-}
> 
> module Understanding.Types where
> 
> import GHC.TypeLits
> 
> data T p (size ∷ Nat) where
>   TZ ∷ T p 0
>   TS ∷ (Show p, (m + 1) ~ n) ⇒
>     { payload ∷ p
>     , next    ∷ T a m } → T a n
> deriving instance Show p ⇒ Show (T p s)
> 
> class MeasuredMonoid a where
>   mmempty  ∷ a 0
>   mmappend ∷ a n → a m → a (n + m)
> 
> instance MeasuredMonoid (T p) where
>   mmempty    = TZ
>   mmappend     TZ         TZ      = TZ
>   mmappend     TZ      t@(TS _ _) = t
>   mmappend  t@(TS _ _)    TZ      = t
>   mmappend tl@(TS pl nl)  tr      = TS pl $ mmappend nl tr
> 
> (<>) ∷ MeasuredMonoid a ⇒ a n → a m → a (m + n)
> (<>) = mmappend

-- * Success, due to use of OPTIONS_GHC -fplugin GHC.TypeLits.Normalise
-- > :t TZ <> TZ
-- TZ <> TZ :: T p 0
-- > TS 1 TZ <> TS 0 TZ
-- TS {payload = 1, next = TS {payload = 0, next = TZ}}
-- > :t TS 1 TZ <> TS 0 TZ
-- TS 1 TZ <> TS 0 TZ :: T a 2

Thank you, everybody!

-- 
take care,
Kosyrev Serge