I have the following class representing categories where the object class is represented by a kind, and each hom class is represented by a type indexed by types of the aforementioned kind.
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds #-}
type Hom o = o -> o -> *
class GCategory (p :: Hom o)
where
gid :: p a a
gcompose :: p b c -> p a b -> p a c
a simple example of an instance is:
instance GCategory (->)
where
gid = id
gcompose = (.)
Now I want to model product categories. As a simple starting point, here's a type modeling the morphisms of a category corresponding to a product of -> with itself:
data Bifunction ab cd
where
Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)
here's the corresponding operations:
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
bifunction_compose :: Bifunction '(b, b') '(c, c') -> Bifunction '(a, a') '(b, b') -> Bifunction '(a, a') '(c, c')
bifunction_compose (Bifunction f1 g1) (Bifunction f2 g2) = Bifunction (f1 . f2) (g1 . g2)
but when I try to stick the operations into an instance of the class:
instance GCategory Bifunction
where
gid = bifunction_id
gcompose = bifunction_compose
I run into the following issue:
• Couldn't match type ‘a’ with ‘'(a0, a'0)’
‘a’ is a rigid type variable bound by
the type signature for:
gid :: forall (a :: (*, *)). Bifunction a a
at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3-5
Expected type: Bifunction a a
Actual type: Bifunction '(a0, a'0) '(a0, a'0)
• In the expression: bifunction_id
In an equation for ‘gid’: gid = bifunction_id
In the instance declaration for ‘GCategory Bifunction’
• Relevant bindings include
gid :: Bifunction a a
(bound at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3)
I believe the important part of the message is the following:
Expected type: Bifunction a a
Actual type: Bifunction '(a0, a'0) '(a0, a'0)
specifically that it can't unify the type forall x y. Bifunction '(x, y) '(x, y) with the type forall (a :: (*, *)). Bifunction a a.
Stripping away most of the domain specific stuff, we're left with the following minimal repro of the problem:
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes #-}
module Repro where
data Bifunction ab cd
where
Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
bifunction_id' :: Bifunction a a
bifunction_id' = bifunction_id
Is there a way I can unify bifunction_id with bifunction_id' above?
An alternative approach I've tried is to use type families, but that still doesn't completely solve the problem:
{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes, TypeFamilies #-}
module Repro where
type family Fst (ab :: (x, y)) :: x
where
Fst '(x, y) = x
type family Snd (ab :: (x, y)) :: y
where
Fst '(x, y) = y
data Bifunction ab cd = Bifunction (Fst ab -> Fst cd) (Snd cd -> Snd cd)
bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id
-- This still doesn't work
-- bifunction_id' :: Bifunction a a
-- bifunction_id' = bifunction_id
-- But now I can do this successfully
bifunction_id' :: Bifunction a a
bifunction_id' = Bifunction id id
But I don't really understand why this identical expression works, and would rather not have to manage a somewhat non obvious distinction like this throughout the rest of the code.
forall (x :: k) (y :: l). p '(x, y) is less general than forall (a :: (k, l)). p a, mainly because there are things of kind (k, l) which are not pairs.
type family NotAPair :: () -> () -> () -> (k, l)
(Note that the type family has no parameters, it's not the same as NotAPair (u :: ()) (v :: ()) (w :: ()) :: ()). If NotAPair '() '() '() :: (k, l) were actually a pair '(,) x y, then we would have this nonsense: '(,) ~ NotAPair '(), x ~ '(), y ~ '().
See also Computing with impossible types https://gelisam.blogspot.com/2017/11/computing-with-impossible-types.html
And even if "all things of kind (k, l) are pairs", there are different ways to make that fact available in the language. If you make it implicit, so that you could for example implicitly convert a forall x y. p '(x, y) into a forall a. p a, you may (or may not) make typechecking undecidable. If you make it explicit, you will have to work to write that conversion (that's Coq for example).