Restricted Monoid type values composition

Question

I have a data type that is an instance of Monoid so I can get nice values composition:

data R a = R String (Maybe (String → a))

instance Monoid (R a) where
  mempty = R "" Nothing
  R s f `mappend` R t g = R (s ++ t) (case g of Just _ → g; Nothing → f)

Next, I don't want to combine all R a values with one another, it doesn't make sense in my domain. So I introduce phantom type t:

{-# LANGUAGE DataKinds, KindSignatures #-}

data K = T1 | T2
data R (t ∷ K) a = R String (Maybe (String → a))

instance Monoid (R t a) where …

So I have "restricted" values:

v1 ∷ R T1 Int
v2 ∷ R T2 Int
-- v1 <> v2 => type error

and "unrestricted":

v ∷ R t Int
-- v <> v1 => ok
-- v <> v2 => ok

But now I have a problem. When it comes to v30, for example:

• I would have huge datakind declaration (data K = T1 | … | T30). I could solve by using type level naturals to get infinite source of phantom types (the cure is worse than the disease, isn't it?)
• I should remember which phantom type for what value to use when writing type signatures in dependent code (that is really annoying)

Is there an easier approach to restrict composition somehow?

Answer 1

Looking for the ConstrainedMonoid

I came to a very similar problem lately, which I finally solved the way described at the end of this post (not involving a monoid, but using predicates on types). However, I took the challenge and tried to write a ConstrainedMonoid class.

Here's the idea:

class ConstrainedMonoid m where
  type Compatible m (t1 :: k) (t2 :: k) :: Constraint
  type TAppend m (t1 :: k) (t2 :: k) :: k
  type TZero m :: k

  memptyC :: m (TZero m)
  mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t')

Ok, there's the trivial instance, which in fact doesn't add anything new (I swapped Rs type arguments):

data K = T0 | T1 | T2 | T3 | T4
data R a (t :: K) = R String (Maybe (String -> a))

instance ConstrainedMonoid (R a) where
  type Compatible (R a) T1 T1 = ()
  type Compatible (R a) T2 T2 = ()
  type Compatible (R a) T3 T3 = ()
  type Compatible (R a) T4 T4 = ()
  type Compatible (R a) T0 y = ()
  type Compatible (R a) x T0 = ()

  type TAppend (R a) T0 y = y 
  type TAppend (R a) x T0 = x
  type TAppend (R a) T1 T1 = T1
  type TAppend (R a) T2 T2 = T2
  type TAppend (R a) T3 T3 = T3
  type TAppend (R a) T4 T4 = T4
  type TZero (R a) = T0

  memptyC = R "" Nothing
  R s f `mappendC` R t g = R (s ++ t) (g `mplus` f)

This unfortunately takes a lot of redundant type instances (OverlappingInstances don't seem to work for type families), but I think it satisfies the monoid laws, at type level as well as at value level.

However, it is not closed. It's more like a set of different monoids, indexed by K. If that's what you want, it should suffice.

If you want more

Let's look at a different variant:

data B (t :: K) = B String deriving Show

instance ConstrainedMonoid B where
  type Compatible B T1 T1 = ()
  type Compatible B T2 T2 = ()
  type Compatible B T3 T3 = ()
  type Compatible B T4 T4 = ()

  type TAppend B x y = T1
  type TZero B = T3 

  memptyC = B ""
  (B x) `mappendC` (B y) = B (x ++ y)

This could be a case which makes sense in your domain -- however, it is not a monoid anymore. And if you tried to make one of it, it'll get the same as the instance above, just with different TZero. I'm actually just speculating here, but my intuition tells me that the only valid monoid instances are exactly the ones like for R a; only with different unit values.

Otherwise, you'll end up with something not neccessarily associative (and probably with a terminal object, I think), which is not closed under composition. And if you want to restrict composition to equal Ks, you'll lose the unit value.

A better way (IMHO)

Here's how I actually solved my problem (I didn't even think of monoids back then, since they didn't make sense anyhow). The solution essentially strips off everything except the Compatible "constraint producer", which is left as a predicate on two types:

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 T1 = ()
type instance Matching T2 T1 = ()
type instance Matching T1 T2 = ()
type instance Matching T4 T4 = ()

used like

foo :: (Matching a b) => B a -> B b -> B Int

This gives you full control over your definition of compatibility, and what kind of composition (not necessarily monoidal) you want, and it is more general. It can be expanded to infinite kinds, too:

-- pseudo code, but you get what I mean
type instance NatMatching m n = (IsEven m, m > n)

---

Answering your two last points:

• Yes, you have to define sufficiently many types in your kind. But I think that they should be self-explaining anyway. You could also split up them into groups, or define a recursive type.

• You mainly have to remind the meaning of the index type at two places: the definition of the constraint, and maybe for factory methods (mkB1 :: String -> B T1). But I think that shouldn't be the problem, if the types are named well. (It can be very redundant, though -- I've not found a way to avoid that yet. Probably TH would work.)

Could this be easier?

What I'd actually like to be able to write is the following:

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 y = ()
type instance Matching x T1 = ()
type instance Matching x y = (x ~ y)

I fear this has a serious reason not to be allowed; however, maybe, it's just not implemented...

EDIT: Nowadays, we have closed type families, which do exactly this.