[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Size-indexed monoids
From:       Hiromi ISHII <konn.jinro () gmail ! com>
Date:       2017-02-23 3:46:37
Message-ID: 526A4BC4-156E-492D-A5AF-F5F2351F3090 () gmail ! com
[Download RAW message or body]

[Attachment #2 (multipart/signed)]


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@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@gmail.com
筑波大学数理物質科学� �究科
数学専攻 博士後期課程一年
----------------------------------------------

> 2017/02/23 0:34、Kosyrev Serge <skosyrev@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@gmail.com
筑波大学数理物質科学� �究科
数学専攻 博士後期課程一年
----------------------------------------------


["signature.asc" (signature.asc)]

-----BEGIN PGP SIGNATURE-----
Comment: GPGTools - https://gpgtools.org

iQEcBAEBCgAGBQJYrlsdAAoJECJklzwRFfjq7VQH/2yrYUUwUomjmAqKoGKYJOf2
2RnWRClyDoMY68x/uClYLblePCZiqN+exz5Z4Mc5aT1fbE/VPRW803wt6ogibvrg
J6rhCdjO7Cm9MFv3xT9P55gcxLwWAHnIGJqgwgMNs4rAIBAQ9Di0Bu7oj3BngVBu
SQcSHmbJQOXqYADZfptipU40xhTgzT5bVNOolAtpBjs8upK/pitdFSdzObgBpm8B
1I6wgx2cJCu9PchzOQ7+9sTjQHl3j3VEDya81nQk8jeS20RdVW3YpxopbouP34M/
Zn/+ySuhV0lcJ6J1fkc5V3JJ8B4RFho6WWprzCBGMjbeRFMmN1KCWw0nmxNDnqE=
=l6iV
-----END PGP SIGNATURE-----

[Attachment #6 (text/plain)]

_______________________________________________
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.

[prev in list] [next in list] [prev in thread] [next in thread]