Size-indexed monoids

older
CFP: International Workshop on OCL...

Kosyrev Serge

22 Feb 2017 22 Feb '17

10:34 a.m.

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

Show replies by date

Ertugrul Söylemez

22 Feb 22 Feb

11:49 a.m.

...

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.

Ertugrul Söylemez

11:53 a.m.

...

{-# LANGUAGE FlexibleContexts #-}

Scratch that one.

Sergey Kosyrev

3:39 p.m.

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

Adam Gundry

4:35 p.m.

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/

Sergey Kosyrev

6 p.m.

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

Li-yao Xia

6:58 p.m.

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.... Li-yao On 02/22/2017 04:35 PM, Adam Gundry 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

On 22/02/17 20:39, Sergey Kosyrev wrote: 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

Hiromi ISHII

10:46 p.m.

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

3009

Age (days ago)

3010

Last active (days ago)

List overview

Download

7 comments

6 participants

participants (6)

Adam Gundry
Ertugrul Söylemez
Hiromi ISHII
Kosyrev Serge
Li-yao Xia
Sergey Kosyrev