Constraining instances

Question

Lets say we've got the following:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilyDependencies #-}

type family CategoryLikeT p_a_b = t | t -> p_a_b

type IsCategoryLike p t a b = (t ~ CategoryLikeT (p, a, b))

class CategoryLike p where
  (>>>) :: 
    (
      IsCategoryLike p t1 a b, 
      IsCategoryLike p t2 b c, 
      IsCategoryLike p t3 a c
    ) => t1 -> t2 -> t3

We then find that this compiles fine:

f :: 
  (
    CategoryLike p, 
    IsCategoryLike p t1 a b, 
    IsCategoryLike p t2 b c, 
    IsCategoryLike p t3 c d, 
    IsCategoryLike p t4 a d
  ) => t1 -> t2 -> t3 -> t4
f x y z = x >>> y >>> z

But we haven't defined any instances yet. Lets do that:

data BasicFunction
type instance CategoryLikeT (BasicFunction, a, b) = a -> b

instance CategoryLike BasicFunction where
  (>>>) = flip (.)

But also "Ints" under addition are kind of category like, if we just assume "a" and "b" are both Void, for example: data BasicInt type instance CategoryLikeT (BasicInt, Void, Void) = Int

instance CategoryLike BasicFunction where
  (>>>) = (+)

Of course the above doesn't work, because there's no constraints on "a" or "b" in the instance definition, so there's no guarentee >>> gets all the same type, hence (+) is not general enough. So what I considered is doing the following:

Firstly, adding a constraint type:

type family CategoryConstraints p t a b

And then adding to the definition of IsCategoryLike like the following:

type IsCategoryLike p t a b = 
  (t ~ CategoryLikeT (p, a, b), CategoryConstraints p t)

We can then add the following constraint:

type instance CategoryConstraints BasicInt t = (t ~ Int)

But now we have a problem. f no longer works, giving this error:

Could not deduce: CategoryConstraints p (CategoryLikeT (p, a, c)))

We can fix this in two ways:

Firstly, by adding IsCategoryLike p t5 a c to the constraints in f. But this could get very messy quickly for more complex functions, you'd have to add a constraint for each operation. Also trivial changes, like changing (x >>> y) >>> z to x >>> (y >>> z) require a change in the signature, which wasn't required when one did not have the constraints.

Alternatively, the type signature could be omitted entirely, or partial type signatures could be used.

However, I'd like to retain full type signatures without then growing and being hard to maintain. Can people suggest alternate approaches?

Answer 1

Hmmm... I'm not sure this is the best approach, but here is a direct improvement of what you have. In particular, I think using associated types makes things cleaner...

{-# LANGUAGE TypeFamilies, 
             ConstraintKinds,
             FlexibleInstances,
             TypeFamilyDependencies #-}

import GHC.Exts (Constraint)

class CategoryLike p where
  type CategoryLikeT p a b = t | t -> p a b
  type CategoryConstraints p a b :: Constraint
  type CategoryConstraints p a b = ()
  (>>>) :: (CategoryConstraints p a b, CategoryConstraints p b c, CategoryConstraints p a c) 
    => CategoryLikeT p a b -> CategoryLikeT p b c -> CategoryLikeT p a c

data BasicFunction
instance CategoryLike BasicFunction where
  type CategoryLikeT BasicFunction a b = a -> b
  (>>>) = flip (.)

data BasicInt
instance CategoryLike BasicInt where
  type CategoryLikeT BasicInt Int Int = Int
  type CategoryConstraints BasicInt a b = (a ~ Int, b ~ Int)
  (>>>) = (+)

So, this is what f looks like now: (I'm writing it with an explicit forall because that makes it a candidate for using TypeApplications)

f :: forall p a b c d. (
    CategoryLike p,
    CategoryConstraints p a b,
    CategoryConstraints p b c,
    CategoryConstraints p a c,
    CategoryConstraints p a d,
    CategoryConstraints p d b
  ) => CategoryLikeT p a d -> 
       CategoryLikeT p d b ->
       CategoryLikeT p b c ->
       CategoryLikeT p a c
f x y z = x >>> y >>> z

To use it, I can do something like this (which looks surprisingly nice):

ghci> :set -XTypeApplications
ghci> :t f @BasicFunction (+1) id show
f @BasicFunction (+1) id show :: (Show a, Num a) => a -> [Char]
ghci> :t f @BasicInt 1 2 3
f @BasicInt 1 2 3 :: Int