是否有可能'解决'一个量词量词？

Question

假设我们有一个类型构造函数f,它通过一个DataKinds提升的对来获得两种类型.

forall (f :: (ka, kb) -> *)

然后我就可以实现一个功能forward,这就好比curry为forall量词:

forward :: forall (f :: (ka, kb) -> *).
           (forall (ab :: (ka, kb)).     f ab) ->
           (forall (a :: ka) (b :: kb).  f '(a, b))
forward x = x

但是,反向功能存在问题:

backward :: forall (f :: (*, *) -> *).
            (forall (a :: *) (b :: *). f '(a, b)) ->
            (forall (ab :: (*, *)). f ab)
backward x = x

GHC 8.0.1给出错误消息:

    • Couldn't match type ‘ab’ with ‘'(a0, b0)’
      ‘ab’ is a rigid type variable bound by
        the type signature for:
          backward :: forall (ab :: (*, *)). (forall a b. f '(a, b)) -> f ab
        at :6:116
      Expected type: f ab
        Actual type: f '(a0, b0)
    • In the expression: x
      In an equation for ‘backward’: backward x = x

从概念上讲,它似乎是一个有效的程序.有没有其他方法来实现这个功能？或者这是GHC的已知限制？

Answer 1

正如Pigworker和Daniel Wagner所指出的那样,问题ab可能是"卡住了".你有时可以使用类型系列解决这个问题(正如我在pigworker的论文中所学到的):

type family Fst (x :: (k1, k2)) :: k1 where
  Fst '(t1, t2) = t1

type family Snd (x :: (k1, k2)) :: k2 where
  Snd '(t1, t2) = t2

backward :: forall (f :: (*, *) -> *) (ab :: (*, *)) proxy .
            proxy ab ->
            (forall (a :: *) (b :: *). f '(a, b)) ->
            f '(Fst ab, Snd ab)
backward _ x = x

有时,另一种选择是使用包装器.

newtype Curry f x y = Curry (f '(x,y))

data Uncurry f xy where
  Uncurry :: f x y -> f '(x, y)