Quantified Constraints for Higher-kinded Typeclasses

Question

Suppose I would like to write two Typeclasses. Header:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Complex

The first typeclass ExClass was defined as such:

class (forall a. (Monoid (t a))) => ExClass t where
    exFunc :: [t (Complex a)] -> t (Complex a)
    exFunc = mconcat -- the actual function is more complicated
    exFunc2 :: (RealFloat a) => t (Complex a) -> a

I defined it as a higher-kinded typeclass because one of its functions' output type depends on the type of its nested value a. I would also like to have a default implementation for exFunc, but it involves the assumption that t a is a Monoid. Now I would like to write an instance for the following type:

newtype ExType a = ExType a

ExType a is a Monoid only when Num a is true:

instance (Num a) => Semigroup (ExType a) where
    ExType a <> ExType b = ExType (a * b)
instance (Num a) => Monoid (ExType a) where
    mempty = ExType 1

Now I go on to define the typeclass instance for ExClass, specifying the constraint of Num a:

instance (forall a. Num a) => ExClass ExType where
    exFunc2 (ExType a) = magnitude a

The above code will compile with no problem. However, if I were to try to use the implemented function like so:

x = ExType 2 :: ExType (Complex Double)

func = exFunc2 x

I receive the following complaint:

• No instance for (Num a) arising from a use of ‘exFunc2’
  Possible fix: add (Num a) to the context of a quantified context
• In the expression: exFunc2 x
  In an equation for ‘func’: func = exFunc2 x

This also happens when I use a different instance declaration:

instance (forall a. Monoid(ExType a)) => ExClass ExType where
    exFunc2 (ExType a) = magnitude a

Is there a way to make this typeclass work? or am I just not supposed to structure my program like this at all?

Answer 1

Daniel Wagner has already explained in his answer the problems with the current definition.

It seems that you want ExClass to mean something like "a class of container types that have a special relationship with another class c applied to their elements, and when their elements satisfy c, the containers themselves are monoids".

For example: ExType has a special relationship with Num. When the elements a of ExType satisfy Num, ExType a becomes a Monoid.

(This is already affirmed in ExTypes Monoid instance, but it seems you want to express it with a higher level of abstraction; to have a class for those containers that become monoids in a similar way.)

In Haskell, there are various possible ways to express a relationship between two types—or between a type and a Constraint. Let's use MultiParameterTypeClasses:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ConstraintKinds #-}

import Data.Kind (Type, Constraint)
-- This kind signature is not strictly required, but makes things clearer
type ExClass :: (Type -> Constraint) -> (Type -> Type) -> Constraint
class (forall a . c a => Monoid (t a)) => ExClass c t | t -> c where
    exFunc :: c a => [t a] -> t a
    exFunc = mconcat 

Notice that ExClass has now two parameters, and that the type f of the container determines (through a functional dependency) the constraint c that is required of the elements of f for f to be a Monoid. c might be different for different fs!

The Semigroup and Monoid instances for ExType don't change. The ExClass instance for ExType would now be:

instance ExClass Num ExType where
    exFunc = mconcat

Putting it to work:

main :: IO ()
main = print $ exFunc [ExType (1::Int), ExType 2]

(I have left out the Complex datatype, which might throw another wrench in the definition.)

Answer 2

I think there's a couple reasoning errors going on here at once.

First: when you write

class (forall a. Monoid (t a)) => ExClass t

this means that if somebody wants to implement an ExClass t instance, then they must show that there is an instance of the form instance Monoid (t a) where ... with no constraints whatsoever on a. Note also that it is not enough for there to be instances for all possible choices of a -- the instance itself must be parametric.

Second: when you write

instance (forall a. Num a) => ExClass ExType

there is no magical connection between the a mentioned here and the a mentioned in the definition of ExClass.

Third: when you write

instance (forall a. Num a) => ExClass ExType

this doesn't actually make an instance of ExClass ExType yet. It makes an instance conditioned on a proof that forall a. Num a. In general, the meaning of instance Ctx => C t is that anybody who wants to assume the fact C t must be able to themselves prove Ctx. Nobody's going to reasonably be able to show forall a. Num a, so this instance is unusable.

These last two comments apply essentially unchanged to your second attempt,

instance (forall a. Monoid(ExType a)) => ExClass ExType

Unfortunately, without more details on what you're trying to do and why, it's nigh-on impossible to suggest the right route forward. Possibilities include an indexed-monad-like approach, moving the class constraint from the class context to various method contexts, not making a class at all, and more.

Answer 3

I would also like to have a default implementation for exFunc, but it involves the assumption that t a is a Monoid

You only require Monoid (t a) in order to have a default implementation? That's backwards. If that constraint isn't conceptually required as a superconstraint for ExClass, then it shouldn't be in the class head.

You can still have a default implementation that is more restrictive:

{-# LANGUAGE DefaultSignatures #-}

class ExClass t where
  exFunc :: [t (Complex a)] -> t (Complex a)
  default exFunc :: Monoid (t (Complex a)) => [t (Complex a)] -> t (Complex a)
  exFunc = mconcat
  exFunc = mconcat -- the actual function is more complicated
  exFunc2 :: (RealFloat a) => t (Complex a) -> a

And then simply

instance ExClass ExType where
  exFunc2 (ExType a) = magnitude a

You would still also be able to provide instances that don't fulfill the Monoid constraint at all, you just then would need to manually implement exFunc too.

Even simpler is to not bother with default implementations at all, but just provide a helper that can be used to get a simple implementation without duplicating any code:

class ExClass t where
  exFunc :: [t (Complex a)] -> t (Complex a)
  exFunc = mconcat -- the actual function is more complicated
  exFunc2 :: (RealFloat a) => t (Complex a) -> a

monoidIshExFunc :: Monoid (t (Complex a)) => [t (Complex a)] -> t (Complex a)
monoidIshExFunc = mconcat

instance ExClass ExType where
  exFunc = monoidIshExFunc
  exFunc2 (ExType a) = magnitude a

(monoidIshExFunc could even require ExClass t, just obviously you should be careful to not end up in a circular definition!)