[Haskell-cafe] Size-indexed monoids

[Sergey Kosyrev]

Ertugrul, all,

I apologize in advance for replying using a lowly MUA, but such are my circumstances..

Ertugrul, first of all, thank you for sharing your approach!

I have tried to replicate your success using GHC.TypeLits.Nat, and I have failed.

The suspicion is that it is due to the fact that, while seductive to use (esp. due to TypeOperators),
TypeLits.Nat carries no inductive proof of structure, which, on the other hand you have provided
with the bespoke TMonoid-associated type families.

Does anybody know if this can be overcome with the current state of art of GHC type-level machinery,
or that we are, indeed, condemned to use the (somewhat) ugly-ish explicitly-inductive numerals?

I remember people seeking to employ GHC plugins to make it more conducive to type-level
arithmetics, but I don't really feel confident to derive judgements about their relevance and
implications on the case..

Here is the record of my failure:

> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, TypeInType, TypeOperators, UnicodeSyntax, StandaloneDeriving #-}
>
> module Understanding.Types where
> 
> import GHC.TypeLits
> import GHC.Types (Type)
> 
> data T p (size ∷ Nat) where
>   TZ ∷ T p 0
>   TS ∷ (Show p, CmpNat (m + 1) n ~ EQ) ⇒
>     { 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

-- * Failure due to lack of inductive structure of GHC.TypeLits.Nat
--
-- error:
--     • Could not deduce: CmpNat ((m1 + m) + 1) (n + m) ~ 'EQ
--         arising from a use of ‘TS’
--       from the context: (Show p1, CmpNat (m1 + 1) n ~ 'EQ)
--         bound by a pattern with constructor:
--                    TS :: forall k (a :: k) (n :: Nat) p (m :: Nat).
--                          (Show p, CmpNat (m + 1) n ~ 'EQ) =>
--                          p -> T a m -> T a n,
--                  in an equation for ‘mmappend’
--         at /home/deepfire/src/haskell-understanding/Types.hs:24:16-23
--     • In the expression: TS pl
--       In the expression: TS pl $ mmappend nl tr
--       In an equation for ‘mmappend’:
--           mmappend tl@(TS pl nl) tr = TS pl $ mmappend nl tr
--     • Relevant bindings include
--         tr :: T p m
--           (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:27)
--         nl :: T p m1
--           (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:22)
--         tl :: T p n
--           (bound at /home/deepfire/src/haskell-understanding/Types.hs:24:12)
--         mmappend :: T p n -> T p m -> T p (n + m)
--           (bound at /home/deepfire/src/haskell-understanding/Types.hs:21:3)

--
take care,
Kosyrev Serge