
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
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
のメール: 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 筑波大学数理物質科学研究科 数学専攻 博士後期課程一年 ----------------------------------------------