`type Object k a :: Constraint` vs `type Object k :: Type -> Constraint`?

[freckletonj]

I was wondering if you could comment on this design decision?

I noticed Conal Elliot went with type Object k :: Type -> Constraint in concat

And this library chooses type Object k a :: Constraint (line #).

I'm just curious what trade-offs you've noticed/anticipated?

EDIT: interestingly, Conal has an experiment with the same Object you use in this lib.

[leftaroundabout]

It's a tradeoff. With

type Object k a :: Constraint

it's easier to define instances. For example you can just list multiple constraints, like

data FooCat a b = ...
instance Category FooCat where
  type Object FooCat a = (Ord a, IsString (Maybe a))

Can't do that with type Object k :: Type -> Constraint, you would first need to define a named class expressing the constraint. (A Constraint-valued type synonym wouldn't do, not even with -XLiberalTypeSynonyms.)

On the flip side, type Object k :: Type -> Constraint allows you to mention Object FooCat by itself. That in turn is not possible with my version. Theoretically it could be achieved by defining (just once and for all!)

class Object k a => Object' k a
instance Object k a => Object' k a

however that requires -XUndecidableSuperClasses, an extension I'm still not completely confident about.

[freckletonj]

Interesting. Those basics of it make sense, and I think I need to just use it a bit more to gain the proper intuitions.

Relatedly, I just chatted with @sellout and discovered he has a category library that makes yet another design tradeoff here, for non-associated type families:

https://github.com/sellout/haskerwaul/blob/master/src/Haskerwaul/Object.hs#L24

type family Ob (c :: ok -> ok -> Type) :: ok -> Constraint

-- ex:
type instance Ob (->) = All

type instance Ob (FullSubcategory ob c) = CFProd (Ob c) ob -- Haskerwaul.Subcategory.Full

newtype FullSubcategory (ob :: ok -> Constraint) (c :: ok -> ok -> Type) a b =
  FS { runFS :: a `c` b }

I think this point is so important to me because the constraints on categories are the novelty that drew me away from base.Category, and there are a few adjacent, but subtly different options on offer. I find Conal's version frustrating to work with, where as your library's choice just tends to work better, but, again, I'm still learning, so it could just be that too.

[leftaroundabout]

That should be very similar to Conal's associated family in practice. It's just that sellout's version the Category class is not supposed to be instantiated directly, so it also can't have an associated type family.