[Haskell-cafe] Size-indexed monoids

[Hiromi ISHII]

Oops, I sent this directly to Kosyrev... I resent this to cafe for the sake of knowledge sharing.
(Sorry Kosyrev for recieving the same message twice...)

---

Hi,

I once write `sized` package, which wraps ListLike functors instead of Monoids:

http://hackage.haskell.org/package/sized

This can be indexed both with peano numeral and GHC.TypeLits.Nat.
To get the latter working, I use several GHC Plugins.


> On 2017/02/23 0:34, Kosyrev Serge <skosyrev at ptsecurity.com> wrote：
> 
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

----- 石井 大海 ---------------------------
konn.jinro at gmail.com
筑波大学数理物質科学研究科
数学専攻 博士後期課程一年
----------------------------------------------

> 2017/02/23 0:34、Kosyrev Serge <skosyrev at ptsecurity.com> のメール：
> 
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

----- 石井 大海 ---------------------------
konn.jinro at gmail.com
筑波大学数理物質科学研究科
数学専攻 博士後期課程一年
----------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170223/bbd3d280/attachment.sig>