I’m working on constrained categories, and I want to write the following:
type Category :: (k -> k -> Type) -> Constraint
class Category cat where
type Objects cat (x :: k) :: Constraint
type Objects cat x = ()
id :: (Objects cat x) => cat x x
(.) ::
(Objects cat x, Objects cat y, Objects cat z) => cat y z -> cat x y -> cat x z
instance Category (->) where
id :: x -> x
id x = x
(.) :: (y -> z) -> (x -> y) -> x -> z
y_z . x_y = \x -> y_z (x_y x)
That’s all well and good, but then I encountered an undocumented error while trying to extend this to natural transformations:
type Transform ::
(k -> k -> Type) ->
(j -> k) ->
(j -> k) ->
Type
newtype Transform cat f g = Transform
{transform :: forall x. cat (f x) (g x)}
instance (Category cat) => Category (Transform cat) where
type Objects (Transform cat) f = forall x. Objects cat (f x) -- GHC-91510
id :: Transform cat f f
id = Transform id
(.) :: Transform cat g h -> Transform cat f g -> Transform cat f h
Transform g_h . Transform f_g = Transform (g_h . f_g)
The error text is
• Illegal polymorphic type: forall (x :: k2). Objects cat (f x)
• In the type instance declaration for ‘Objects’
In the instance declaration for ‘Category (Transform cat)’
Why is this polymorphic type illegal? It’s just a quantified constraint. What can be done to legalize it?
If you extract it to a type synonym you get a more informative error message:
type Foo :: (k -> k -> Type) -> (k -> Type) -> Constraint
type Foo cat f = forall x. Objects cat (f x)
T2.hs:28:1: error: [GHC-02550]
• Quantified predicate must have a class or type variable head:
forall (x :: k). Objects cat (f x)
• In the quantified constraint ‘forall (x :: k). Objects cat (f x)’
In the type synonym declaration for ‘Foo’
|
28 | type Foo cat f = forall x. Objects cat (f x)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Also reading the GHC Users’ guide, I think a quantified constraint can only have a concrete class or a constraint variable as the head (not the one that is involved in that same quantified constraint though). In your case the head is Objects which is a type family which is not allowed.
This tells me I can’t do this because Objects is a constraint family. The error page for GHC-02550 suggests turning Objects into its own class, but then, how do I turn instance Objects (->) x into, say, Ord x?
type Objects :: Type -> (k -> k -> Type) -> k -> Constraint
class C arr a => Objects c arr a where
type C arr a :: Constraint
data DoOrd
instance Ord a => Objects DoOrd (->) a where
type C _ a = Ord a
type Objects :: Type -> (k -> k -> Type) -> k -> Constraint
class Objects bleh cat (x :: k) where
type ObjectsC cat (x :: k) :: Constraint
type Category :: (k -> k -> Type) -> Constraint
class Category cat where
id :: (Objects bleh cat x) => cat x x
(.) ::
(Objects bleh cat x, Objects bleh cat y, Objects bleh cat z) =>
cat y z -> cat x y -> cat x z
instance Objects bleh (Transform cat) f where
type ObjectsC cat f = () -- GHC-25897
The new error text:
• Expecting one more argument to ‘f’
Expected kind ‘k’, but ‘f’ has kind ‘j -> k’
‘k’ is a rigid type variable bound by
a family instance declaration
However, ObjectsC is indeed expecting f to have kind j -> k.
class Objects cat x => ObjectClass cat x
instance Objects cat x => ObjectClass cat x
class (forall x. f x => g x) => f ==> g
instance (forall x. f x => g x) => f ==> g
infix 2 ==>
class f (g x) => (f . g) x
instance f (g x) => (f . g) x
and a few tweaks to your implementation (which I think are fixes)
type Transform ::
(k -> k -> Type) ->
(j -> k) ->
(j -> k) ->
Type
newtype Transform cat f g = Transform
{transform :: forall x. Objects cat x => cat (f x) (g x)}
instance (Category cat) => Category (Transform cat) where
type Objects (Transform cat) f = ObjectClass cat ==> ObjectClass cat . f
id = Transform id
Transform g_h . Transform f_g = Transform (g_h . f_g)
The tweaks I introduced were an attempt to fix some errors that were actually due to the unconstrained type signatures on id and (.); they aren’t relevant to the core issue here, so technically you can leave Transform unchanged and use
class (forall x. f x) => Universally f
instance (forall x. f x) => Universally f
to declare
instance (Category cat) => Category (Transform cat) where
type Objects (Transform cat) f = Universally (ObjectClass cat . f)
However, those tweaks did point in the right direction semantically: if the true objects of the categories involved are only those satisfying the corresponding Objects constraints, then introducing an unconstrainable x as an object in the field of Transform is erroneous.
That said, imposing the constraint from cat, the target category isn’t right either; that restricts us to transformations between endofunctors. The true fix requires Transform to know about the source category:
type Transform ::
(j -> j -> Type) ->
(k -> k -> Type) ->
(j -> k) ->
(j -> k) ->
Type
newtype Transform src tgt f g = Transform
{transform :: forall x. Objects src x => tgt (f x) (g x)}
instance (Category src, Category tgt) => Category (Transform src tgt) where
type Objects (Transform src tgt) f = ObjectClass src ==> ObjectClass tgt . f
id = Transform id
Transform g_h . Transform f_g = Transform (g_h . f_g)
This was working, but now GHC has decided to spit out an error
type Transform ::
(j -> j -> Type) ->
(k -> k -> Type) ->
(j -> k) ->
(j -> k) ->
Type
newtype Transform c d f g = Transform
{transform :: forall x. (Objects c x) => d (f x) (g x)}
type (-->) = Transform (->) (->)
instance (Category c, Category d) => Category (Transform c d) where
type Objects (Transform c d) f = Objects' c ==> Objects' d . f
id :: (Objects (Transform c d) f) => Transform c d f f
id = Transform id
(.) ::
( Objects (Transform c d) f
, Objects (Transform c d) g
, Objects (Transform c d) h
) =>
Transform c d g h -> Transform c d f g -> Transform c d f h
Transform g_h . Transform f_g = Transform (g_h . f_g) -- GHC-05617
The error text is disappointing:
• Could not deduce: (Objects d (f x), Objects d (g x), Objects d (h x))
arising from a use of ‘.’
from the context: (Category c, Category d)
bound by the instance declaration
or from: (Objects (Transform c d) f, Objects (Transform c d) g,
Objects (Transform c d) h)
bound by the type signature for:
(.) :: forall (f :: j -> k) (g :: j -> k) (h :: j -> k).
(Objects (Transform c d) f, Objects (Transform c d) g,
Objects (Transform c d) h) =>
Transform c d g h -> Transform c d f g -> Transform c d f h
or from: Objects c x
bound by a type expected by the context:
forall (x :: j). Objects c x => d (f x) (h x)
• In the first argument of ‘Transform’, namely ‘(g_h . f_g)’
In the expression: Transform (g_h . f_g)
In an equation for ‘.’:
Transform g_h . Transform f_g = Transform (g_h . f_g)
I switched GHCs from 9.12.2 to 9.14.1 and back, and the error occurred.
type C0 :: k -> Constraint
class C0 x
instance C0 x
type CCompose :: (k -> Constraint) -> (j -> k) -> Constraint
class (forall x. (c (f x))) => CCompose c f
type Category :: (k -> k -> Type) -> Constraint
class Category cat where
type Objects cat :: k -> Constraint -- changed
id :: (Objects cat x) => cat x x
(.) ::
(Objects cat x, Objects cat y, Objects cat z) =>
cat y z -> cat x y -> cat x z
instance (Category c, Category d) => Category (Transform c d) where
type Objects (Transform c d) = CCompose (Objects d) -- nice!
id :: (Objects (Transform c d) f) => Transform c d f f
id = Transform id
(.) ::
( Objects (Transform c d) f
, Objects (Transform c d) g
, Objects (Transform c d) h
) =>
Transform c d g h -> Transform c d f g -> Transform c d f h
Transform g_h . Transform f_g = Transform (g_h . f_g)
Compiles! Thanks for pointing me in the right direction @Leary!
Mmm, indeed—the change to type Objects c :: k -> Constraint seems to be necessary for GHC 9.14 to handle the quantified constraint, though I don’t really know why.
Unrelatedly, you lost the precondition on type Objects (Transform c d); CCompose (Objects d) is too strong. Call me crazy, but how about:
class (Category c, Category d, Objects c ==> ObjectClass d . f)
=> Functor c d f where
map :: a `c` b -> f a `d` f b
instance Category (Transform c d) where
type Objects (Transform c d) = Functor c d
...
I already have a Morphisms class, that only requires a Category constraint on d, in order to allow things like Morphisms (Procompose (Kleisli Maybe) (Indexed i)) (->) for a custom FilterableWithIndex class. I haven’t quite figured out how to put a Category constraint on anything Procompose yet.
class (Category d) => Morphisms c d f where
morphism :: c x y -> d (f x) (f y)
Is this closer to what you’re saying about strength?
type Composed :: (j -> Constraint) -> (k -> Constraint) -> (j -> k) -> Constraint
class (forall x. (g x => c (f x))) => Composed g c f
instance (Category c, Category d) => Category (Transform c d) where
type Objects (Transform c d) = Composed (Objects c) (Objects d)