Nullary operations on GADT with constraints

Learn
1

I am trying to define something similar to Data.Monoid.Ap but as GADT with constraints on the constructors:

import Data.Monoid (Ap(..))
-- instance (Monoid a, Applicative f) => Monoid (Ap f a)

data Lifted f a where
   Lift :: (Monoid a, Applicative f) => Ap f a -> Lifted f a

One can have a Semigroup instance wherein the constraints are hidden:

instance Semigroup (Lifted f a) where
   (Lift a) <> (Lift b) = Lift (a <> b)

This works because by matching on the Lift constructor, the constraints necessary for the Semigroup (Ap f a) instance are brought into scope.
However, this approach does not work for nullary operations like mempty, because there is nothing to pattern-match on. Can it be done nevertheless? Perhaps with proxies?

A possible work-around would be to introduce a second constructor taking a rank-2 argument:

data Lifted f a where
   Lift :: (Monoid a, Applicative f) => Ap f a -> Lifted f a
   Constant :: (forall x. Monoid x => x)       -> Lifted f a

instance Monoid (Lifted f a) where
   mempty = Constant mempty

The drawback is combinatorial explosion in the definition of the semigroup operation (or any other n-ary operation). Instead of one case, it now must handle four.

The class Monoid is only an example. My question applies to all classes of algebraic structures that have constants.

2

This reminds me of Kmett’s type classes vs the world (around 7:48):

He uses the example of fromInteger which suffers from the same issue.

3

You’re bundling constraints with the values, thus requiring them upon construction but not destruction.

If you impose constraints on the values instead, then you’ll need them upon destruction but not construction. That will allow you to produce these values without first matching on another:

newtype Monoidal a where
  MkMonoidal :: (Monoid a => a) -> Monoidal a

instance Semigroup (Monoidal a) where
  MkMonoidal x <> MkMonoidal y = MkMonoidal (x <> y)

instance Monoid (Monoidal a) where
  mempty = MkMonoidal mempty
4

Yes, that is exactly what I described as my work-around: MkMonoidal = Constant.

It turns out the combinatorial explosion is not too bad, because one can reduce binary operations involving constants to unary operations forall a. Monoid a => a -> a.

The only remaining downside is when there are specific class members that identify two constants:

newtype Bounds a where
   Bound :: (Bounded a => a) -> Bounds a

instance Bounded (Bounds a) where
   maxBound = Bound maxBound
   minBound = Bound minBound

We have

minBound == () == maxBound

But minBound :: Bounds () can be distinguished from maxBound :: Bounds () by matching the Bound constructor and casting the value to another non-singleton type.

5

That’s possible for your original Constant approach, but not for this MkMonoidal/Bound approach, because the latter doesn’t put the quantification inside the constructor.

6

Ah, so the difference is

Constant   :: (forall x. Monoid x => x) -> Lifted f a
MkMonoidal :: (          Monoid a => a) -> Monoidal a

so MkMonoidal takes a monomorphic argument. The consequence of this is that Monoidal a is the empty type when a is not already a monoid, whereas Lifted f a always has an inhabitant.
I’ll experiment and see whether the monomorphic variant has any other drawbacks.