将多种类量化变量与元组类型统一起来

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)都是成对的"，也有不同的方法可以在语言中提供这一事实。如果你把它隐式，以便你可以隐式地将一个forall x y. p '(x, y)转换为一个forall a. p a，你可以(或可能不会(使类型检查不可判定。如果你把它明确，你将不得不努力编写该转换(例如Coq(。

Answer 2

在gid @Bifunction的定义中，你有一个类型a :: (Type, Type)。(,)只有一个构造函数，因此我们可以推断出必须存在x :: Type和y :: Type，以至于a ~ '(x, y).然而，这种推理在哈斯克尔中是无法表达的。基本上，当你在 Haskell 中有一个类型级对(类型(i, j)的东西(时，你不能假设它实际上是一对(形式'(x, y)的东西(。这会导致你的代码中断：你有Bifunction id id :: forall x y. Bifunction '(x, y) '(x, y)，但你需要一个Bifunction a a，你只是没有一个打字规则让你假设a ~ (x, y)某些x，y。当你使用Bifunction的替代的、奇怪的定义时，你会得到Bifunction id id :: forall a. Bifunction a a(因为这是构造函数的返回类型(，它基本上是因为Fst和Snd是"部分"函数。

我个人只会添加"所有对实际上是对"作为公理。

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