用元组类型统一多类量化变量

Question

我有以下表示类别的类别，其中对象类别由一种种类表示，每个hom类由一种由上述种类的类型索引的类型表示。

{-# 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

一个实例的简单示例是：

instance GCategory (->)
  where
  gid = id
  gcompose = (.)

现在，我要对产品类别进行建模。作为一个简单的起点，下面是一个类型，它对->与本身的乘积相对应的类别的词素进行建模：

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

但是当我尝试将操作粘贴到类的实例中时：

instance GCategory Bifunction
  where
  gid = bifunction_id
  gcompose = bifunction_compose

我遇到以下问题：

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

我相信消息的重要部分如下：

  Expected type: Bifunction a a
    Actual type: Bifunction '(a0, a'0) '(a0, a'0)

特别是它不能将类型forall x y. Bifunction '(x, y) '(x, y)与类型统一forall (a :: (*, *)). Bifunction a a。

除去大多数特定于域的内容，剩下的问题的最小再现如下：

{-# 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

有什么我可以bifunction_id与bifunction_id'上面统一的方法吗？

---

我尝试过的另一种方法是使用类型族，但这仍然不能完全解决问题：

{-# 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

但是我真的不明白为什么相同的表达式起作用，并且宁愿不必在其余的代码中管理这种不太明显的区别。

Answer 1

forall (x :: k) (y :: l). p '(x, y)比 不那么普遍forall (a :: (k, l)). p a，主要是因为有些事物(k, l)不是成对的。

type family NotAPair :: () -> () -> () -> (k, l)

（请注意，类型族没有参数，它与 不同NotAPair (u :: ()) (v :: ()) (w :: ()) :: ()）。如果NotAPair '() '() '() :: (k, l)实际上是一对'(,) x y，那么我们就会得到这样的废话：'(,) ~ NotAPair '(), x ~ '(), y ~ '()。

另请参阅使用不可能类型进行计算https://gelisam.blogspot.com/2017/11/computing-with-impossible-types.html

即使“所有种类的事物(k, l)都是成对的”，也可以通过不同的方式在语言中表达这一事实。如果将其设为隐式，以便可以将 a 隐式转换forall x y. p '(x, y)为 a forall a. p a，则可以（也可以不）使类型检查变得不可判定。如果您将其明确化，则必须编写该转换（例如 Coq）。