4

假设我们有一个类型构造函数 f，它通过一个 DataKinds-promoted 对来接受两种类型。

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

然后我可以实现一个函数，forward就像量词一样：curryforall

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 给出错误消息：

    • 无法将类型 'ab' 与 ''(a0, b0)' 匹配
      'ab' 是一个刚性类型变量，由
        类型签名：
          向后 :: forall (ab :: (*, *))。(forall a b. f '(a, b)) -> f ab
        在:6:116
      预期类型：f ab
        实际类型：f '(a0, b0)
    • 在表达式中：x
      在“向后”的方程中：向后 x = x

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

4

1 回答 1

6

正如 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)
于 2016-09-06T18:46:24.537 回答