Unifying polykinded quantification variable with tuple kinded type

Question

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.

Answer 1

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).

Answer 2

In gid @Bifunction's definition, you have a type a :: (Type, Type). (,) only has one constructor, so we can deduce that there must exist x :: Type and y :: Type such that a ~ '(x, y). However, this reasoning is not expressible in Haskell. Basically, when you have a type-level pair (something of type (i, j)) in Haskell, you can not assume that it is actually a pair (something of form '(x, y)). This causes your code to break: you have Bifunction id id :: forall x y. Bifunction '(x, y) '(x, y), but you need a Bifunction a a, and you just do not have a typing rule that lets you assume that a ~ (x, y) for some x, y. When you use the alternate, weird definition of Bifunction, then you get Bifunction id id :: forall a. Bifunction a a (because that's the return type of the constructor), and it works basically because Fst and Snd are "partial" functions.

I would personally just add "all pairs are actually pairs" as an axiom.

data IsTup (xy :: (i, j)) =
    forall (x :: i) (y :: j). xy ~ '(x, y) => IsTup
-- could also write
-- data IsTup (xy :: (i, j)) where
--     IsTup :: forall (x :: i) (y :: j). IsTup '(x, y)
isTup :: forall xy. IsTup xy
isTup = unsafeCoerce IsTup

bifunction_id :: Bifunction '(a, x) '(a, x)
bifunction_id = Bifunction id id
bifunction_compose :: Bifunction '(b, y) '(c, z) -> Bifunction '(a, x) '(b, y) -> Bifunction '(a, c) '(x, z)
bifunction_compose (Bifunction fl fr) (Bifunction gl gr) = Bifunction (fl . gl) (fr . gr)

instance GCategory Bifunction where
   gid :: forall a. Bifunction a a -- necessary to bind a
   -- usage of axiom: isTup produces a "proof" that a is actually a pair and
   -- matching against IsTup "releases" the two components and the equality 
   gid | IsTup <- isTup @a = bifunction_id
   gcompose :: forall a b c. Bifunction b c -> Bifunction a b -> Bifunction a c
   gcompose
     | IsTup <- isTup @a, IsTup <- isTup @b, IsTup <- isTup @c
     = bifunction_compose