Search code examples
haskellquantified-constraints

Quantified Constraints for Higher-kinded Typeclasses


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?


Solution

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