为什么ghc不能在这个Category产品上匹配这些类型？

Question

我有一个很典型的定义，就是这样一个类别。

class Category (cat :: k -> k -> Type) where
  id :: cat a a
  (.) :: cat a b -> cat c a -> cat c b

现在我想把 产品类别 所以我做了这个GADT

data ProductCategory
  (cat1 :: a -> a -> Type)
  (cat2 :: b -> b -> Type)
  (x :: (a, b))
  (y :: (a, b))
  where
MorphismProduct :: cat1 x x -> cat2 y y -> ProductCategory cat1 cat2 '(x, y) '(x, y)

现在这个编译得很好，我的问题是，当我试图把它变成一个类似于 Category. 这里的数学真的很简单，看来这应该是一个简单的例子。 所以我得出的结果是这样的。

instance
  ( Category cat1
  , Category cat2
  )
    => Category (ProductCategory cat1 cat2)
  where
    id = MorphismProduct id id
    (MorphismProduct f1 f2) . (MorphismProduct g1 g2) = MorphismProduct (f1 . g1) (f2 . g2)

但结果却出现了一个错误

    • Couldn't match type ‘a2’ with ‘'(x0, y0)’
      ‘a2’ is a rigid type variable bound by
        the type signature for:
          id :: forall (a2 :: (a1, b1)). ProductCategory cat1 cat2 a2 a2
        at src/Galaxy/Brain/Prelude.hs:175:5-6
      Expected type: ProductCategory cat1 cat2 a2 a2
        Actual type: ProductCategory cat1 cat2 '(x0, y0) '(x0, y0)
    • In the expression: MorphismProduct id id
      In an equation for ‘id’: id = MorphismProduct id id
      In the instance declaration for
        ‘Category (ProductCategory cat1 cat2)’
    • Relevant bindings include
        id :: ProductCategory cat1 cat2 a2 a2
          (bound at src/Galaxy/Brain/Prelude.hs:175:5)
    |
175 |     id = MorphismProduct id id
    |          ^^^^^^^^^^^^^^^^^^^^^

我在这个错误上花了很长时间 我不知道它想告诉我什么. 它声称它不能匹配 a 到 '(x0, y0) 但我不知道为什么，好像真的应该可以。

这里遇到的问题是什么？ 如何解决就好了，但我真的很想知道如何阅读这条信息。

Answer 1

id 应该有类型 forall a. MyCat a a 但在这种情况下，你只能构建 forall x y. MyCat '(x, y) '(x, y). 归纳起来，进一步要求假设所有的对子 a :: (t1, t2) 属于 a = '(x, y)，这在Haskell中是无法证明的。

一个变通的办法是不使用 GADT；特别是，不要在构造函数中细化类型参数。取而代之的是

data ProductCategory cat1 cat2 a b where
  Pair :: cat1 x x' -> cat2 y y' -> ProductCategory cat1 cat2 '(x, y) '(x', y')

这样做。

data ProductCategory cat1 cat2 a b where
  Pair :: cat1 (Fst a) (Fst b) -> cat2 (Snd a) (Snd b) -> ProductCategory cat1 cat2 a b

type family Fst (a :: (k1, k2)) :: k1 where Fst '(x, y) = x
type family Snd (a :: (k1, k2)) :: k2 where Snd '(x, y) = y

注意定义 ProductCategory 相当于此，没有GADT语法。

data ProductCategory cat1 cat2 a b
  = ProductCategory (cat1 (Fst a) (Fst b)) (cat2 (Snd a) (Snd b))