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

Question

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

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

但是当我尝试将操作粘贴到 class:

的实例中时

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

在gid @Bifunction的定义中，你有一个类型a :: (Type, Type)。 (,)只有一个构造函数，所以我们可以推断必须存在x :: Type和y :: Type使得a ~ '(x, y)。然而，这个推理在Haskell中是无法表达的。基本上，当你在 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（因为那是构造函数的 return 类型），它之所以有效，基本上是因为 Fst 和 Snd 是 "partial" 函数。

我个人只会添加 "all pairs are actually pairs" 作为公理。

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

Answer 2

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

即使 "all things of kind (k, l) are pairs"，也有不同的方法可以在语言中提供该事实。如果你使它隐式，例如你可以隐式地将 forall x y. p '(x, y) 转换为 forall a. p a，你可能（或可能不会）使类型检查不可判定。如果你明确表示，你将不得不努力编写该转换（例如 Coq）。

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

Unifying polykinded quantification variable with tuple kinded type

haskell

forall

data-kinds

polykinds