haskellcategory-abstractions

Error trying to define type Relation [(a,b)] as an instance of Category class


I'm exploring some possible implementations of R subset of AxB, each with its limits and possibilities. I would also like, when possible, to define them as instances of the Category class or Semigroupoid class.

I have chosen the list of pairs since, with regard to the operation of composing lists, it only places types of the elements of the pair the constraint of being instances of the Eq class.

Now I'm stuck on this compiler error message: "No instance for (Eq a) arising from a use of ‘°’"

What's wrong?

{-# LANGUAGE GADTs #-}

module RelationT where

import Data.List
import Control.Category as Cat

data RelationT a b where
  Id :: RelationT a a
  RT :: (Eq a, Eq b) => [(a,b)] -> RelationT a b

instance Category RelationT where
  id = Id
  Id . r = r
  r . Id = r
  r1 . r2 = r1 ° r2 -- error:  No instance for (Eq a) arising from a use of ‘°’

(°) :: (Eq a, Eq b, Eq t) => RelationT t b -> RelationT a t -> RelationT a b
RT r1 ° RT r2 = RT $ nub $ go r1 r2
    where
    go [] r =  []
    go r [] =  []
    go xys2 ( ((x1,y1): xys1)) =  go2 x1 y1 xys2 [] ++ go xys2  xys1
        where
        go2 x y [] acc = acc
        go2 x y ((w,z):wzs) acc
          | y == w = go2 x y wzs ((x,z):acc)
          | otherwise = go2 x y wzs acc

-- ex. RT [(1,'a'),(4,'b'),(5,'c'),(10,'d')] ° RT [(3,10),(1,5),(1,1)]
-- > RT [(3,'d'),(1,'c'),(1,'a')]

Solution

  • If you're storing the Eq constraints in a GADT, there's no need to require that from the signature: by pattern-matching on the relation-values, the constraint will already be in scope. So, just change the signature to

    (°) :: RelationT t b -> RelationT a t -> RelationT a b
    

    The (Eq a, Eq b, Eq c) information will still be available within the function body, because you've pattern-matched RT r1 and RT r2 there, which if successful witness that all the types have an Eq instance.

    That said: in my experience, this trick of storing a constraint in a GADT leads quickly into trouble when you want to do more involved stuff with your category. The problem is, the standard Category class is not really suitable for a relation type like this, because it only supports categories which have exactly the same objects as Hask – i.e., all Haskell types. But your relation category really has only equality-comparable types as objects; with the extra Id constructor you're forcibly extending it to also include relations between non-eq types, but there only the identity relation is available... that's quite a fragile hack.

    The proper way out is to use a typeclass which allows the categories to have a more restricted notion of objects to begin with. The simplest means to do that are constraint kinds. From my constrained-categories package:

    {-# LANGUAGE TypeFamilies, ConstraintKinds #-}
    import GHC.Exts (Constraint)
    
    class Category k where
      type Object k o :: Constraint
      id :: Object k a => k a a
      (.) :: (Object k a, Object k b, Object k c)
             => k b c -> k a b -> k a c
    

    Then you can make the instance

    data RelationT a b where
      Id :: RelationT a a
      RT :: [(a,b)] -> RelationT a b
    
    instance Category RelationT where
      type Object RelationT o = Eq o
      id = Id
      (.) = (°)