Size-indexed monoids

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Size-indexed monoids

Kosyrev Serge-2
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.
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Ertugrul Söylemez-3
> 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 don't think monoid is the correct term simply because it's indexed.
I've called them measured monoids, and the following approach seems to
work well:

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeInType #-}

    import GHC.Types (Type)

    class TMonoid a where
        type family Empty a :: a
        type family Append a (x :: a) (y :: a) :: a

    data Nat = Z | S Nat

    instance TMonoid Nat where
        type Empty Nat = Z
        type Append Nat Z y = y
        type Append Nat (S x) y = S (Append Nat x y)

    class MeasuredMonoid (a :: n -> Type) where
        mmEmpty  :: a (Empty n)
        mmAppend :: a n1 -> a n2 -> a (Append n n1 n2)

    data Vec :: Type -> Nat -> Type where
        Nil  :: Vec a Z
        Cons :: a -> Vec a n -> Vec a (S n)

    instance MeasuredMonoid (Vec a) where
        mmEmpty = Nil
        mmAppend Nil ys = ys
        mmAppend (Cons x xs) ys = Cons x (mmAppend xs ys)

I couldn't tell you whether there is a library for that though.

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

signature.asc (497 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Ertugrul Söylemez-3
>     {-# LANGUAGE FlexibleContexts #-}

Scratch that one.

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

signature.asc (497 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Kosyrev Serge-2
In reply to this post by Ertugrul Söylemez-3
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
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Adam Gundry-2
On 22/02/17 20:39, Sergey Kosyrev wrote:
> 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 don't believe this is possible without cheating (see below) or using a
plugin. That said, some of the ugliness of inductive numerals can be
avoided by defining a type family to translate TypeLits.Nat into
inductive form.

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

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.

If you'd prefer blatant cheating, another approach is to use
unsafeCoerce, like this:


{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, TypeInType,
             TypeOperators, UnicodeSyntax, StandaloneDeriving,
             TypeApplications, RankNTypes, ScopedTypeVariables,
             AllowAmbiguousTypes, ConstraintKinds #-}

module SizeIndexedMonoids where

import GHC.TypeLits
import GHC.Types (Type)
import Unsafe.Coerce

-- | Assert without proof that the constraint c holds.  It had better
-- be a true type equality constraint, otherwise you are asking for
-- trouble.
unsafeLemma :: forall c r . (c => r) -> r
unsafeLemma = unQ . (unsafeCoerce :: Q c r -> Q (r ~ r) r) . MkQ

newtype Q c r = MkQ { unQ :: c => r }

type Associativity x y z = (x + (y + z)) ~ ((x + y) + z)

data T (p :: Type) (size ∷ Nat) where
  TZ ∷ T p 0
  TS ∷ (Show p, (1 + m) ~ n) ⇒
    { payload ∷ p
    , next    ∷ T a m } → T a n
deriving instance Show p ⇒ Show (T p s)

mmappend :: forall p m n . T p m -> T p n -> T p (m + n)
mmappend TZ tr = tr
mmappend (TS pl (nl :: T a m1)) tr =
    unsafeLemma @(Associativity 1 m1 n) (TS pl (mmappend nl tr))


Sorry,

Adam


> 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

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Kosyrev Serge-2
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
   
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Li-yao Xia-2
In reply to this post by Adam Gundry-2
Hello,

This approach using unsafeCoerce is implemented by the recently added
Data.Constraints.Nat module of the constraints package, which exports
reusable proofs to help GHC reason about type-level literals. It's
definitely something very experimental, and the current version on
Hackage is unfortunately bugged, but seems worth mentioning.

http://hackage.haskell.org/package/constraints-0.9/docs/Data-Constraint-Nat.html

Li-yao

On 02/22/2017 04:35 PM, Adam Gundry wrote:

> On 22/02/17 20:39, Sergey Kosyrev wrote:
>> 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 don't believe this is possible without cheating (see below) or using a
> plugin. That said, some of the ugliness of inductive numerals can be
> avoided by defining a type family to translate TypeLits.Nat into
> inductive form.
>
>> 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..
> 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.
>
> If you'd prefer blatant cheating, another approach is to use
> unsafeCoerce, like this:
>
>
> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, TypeInType,
>               TypeOperators, UnicodeSyntax, StandaloneDeriving,
>               TypeApplications, RankNTypes, ScopedTypeVariables,
>               AllowAmbiguousTypes, ConstraintKinds #-}
>
> module SizeIndexedMonoids where
>
> import GHC.TypeLits
> import GHC.Types (Type)
> import Unsafe.Coerce
>
> -- | Assert without proof that the constraint c holds.  It had better
> -- be a true type equality constraint, otherwise you are asking for
> -- trouble.
> unsafeLemma :: forall c r . (c => r) -> r
> unsafeLemma = unQ . (unsafeCoerce :: Q c r -> Q (r ~ r) r) . MkQ
>
> newtype Q c r = MkQ { unQ :: c => r }
>
> type Associativity x y z = (x + (y + z)) ~ ((x + y) + z)
>
> data T (p :: Type) (size ∷ Nat) where
>    TZ ∷ T p 0
>    TS ∷ (Show p, (1 + m) ~ n) ⇒
>      { payload ∷ p
>      , next    ∷ T a m } → T a n
> deriving instance Show p ⇒ Show (T p s)
>
> mmappend :: forall p m n . T p m -> T p n -> T p (m + n)
> mmappend TZ tr = tr
> mmappend (TS pl (nl :: T a m1)) tr =
>      unsafeLemma @(Associativity 1 m1 n) (TS pl (mmappend nl tr))
>
>
> Sorry,
>
> Adam
>
>
>> 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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Size-indexed monoids

Hiromi ISHII
In reply to this post by Kosyrev Serge-2
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 <[hidden email]> 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.
----- 石井 大海 ---------------------------
[hidden email]
筑波大学数理物質科学研究科
数学専攻 博士後期課程一年
----------------------------------------------

> 2017/02/23 0:34、Kosyrev Serge <[hidden email]> のメール:
>
> 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.
----- 石井 大海 ---------------------------
[hidden email]
筑波大学数理物質科学研究科
数学専攻 博士後期課程一年
----------------------------------------------


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

signature.asc (507 bytes) Download Attachment