如何将 `forall a. a -> a` 转换回 `a -> a`？

Question

在我的实际问题中，我有一个作为参数传递的函数f，它会改变列表中的顺序，但对类型没有要求，也不会改变类型。我想将该函数应用于[Int]和[Bool]，因此必须解决两个上下文，并尝试将f强制转换为[Int] -> [Int]或[Bool] -> [Bool]。我使用Rank2Types解决了这个问题。 但是，当我在像f这样的函数列表上使用any时，any需要函数是[a] -> [a]而不是forall a. [a] -> [a]。下面的代码虽然毫无意义，但完美地重现了这个错误：

{-# LANGUAGE Rank2Types #-}

--debug :: (forall a. [a] -> [a]) -> Bool 
debug swap = any combine [swap]
  where
    combine :: (forall a. [a] -> [a]) -> Bool
    combine f =  usefonBool f && usefonInt f
    --usefonBool :: (forall a. [a] -> [a]) -> Bool
    usefonBool f = f [True,True] == [False]

    --usefonInt :: (forall a. [a] -> [a]) -> Bool
    usefonInt f = (f [1,2]) == [2,1]

错误信息是：

• Couldn't match type ‘a’ with ‘forall a1. [a1] -> [a1]’
  ‘a’ is a rigid type variable bound by
    the inferred type of debug :: a -> Bool
    at /path/debug.hs:(4,1)-(12,36)
  Expected type: a -> Bool
    Actual type: (forall a. [a] -> [a]) -> Bool
• In the first argument of ‘any’, namely ‘combine’
  In the expression: any combine [swap]
  In an equation for ‘debug’:
      debug swap
        = any combine [swap]
        where
            combine :: (forall a. [a] -> [a]) -> Bool
            combine f = usefonBool f && usefonInt f
            usefonBool f = f [True, ....] == [False]
            usefonInt f = (f [1, ....]) == [2, ....]
• Relevant bindings include
    swap :: a (bound at /path/debug.hs:4:7)
    debug :: a -> Bool (bound at /path/debug.hs:4:1)
|

我的目标是找到一种注释方法，它可以让我在不同类型上使用f，并对这些通用函数的列表应用任何操作。

如果我取消所有类型注释（或只取消顶部的注释），错误就会改变为

• Couldn't match type ‘[a0] -> [a0]’ with ‘forall a. [a] -> [a]’
  Expected type: ([a0] -> [a0]) -> Bool
    Actual type: (forall a. [a] -> [a]) -> Bool
• In the first argument of ‘any’, namely ‘combine’
  In the expression: any combine [swap]
  In an equation for ‘debug’:
      debug swap
        = any combine [swap]
        where
            combine :: (forall a. [a] -> [a]) -> Bool
            combine f = usefonBool f && usefonInt f
            usefonBool :: (forall a. [a] -> [a]) -> Bool
            usefonBool f = f [True, ....] == [False]
            ....
  |

- peer

---

你为什么注释掉了类型签名？ - leftaroundabout

@leftaroundabout 我将它们注释掉了，以呈现尽可能少的假设版本。 - peer

它不是那样工作的。 GHC 只能推断出 Rank-1 类型，因此您必须使用显式签名。在这种情况下，顶层签名应该足够了。但无论如何，省略签名通常都是一个坏主意。 - leftaroundabout

@leftaroundabout 取消注释 我的 顶层签名还没有解决它。 - peer

Answer 1

首先，需要注意的是Rank2Types已经不再使用。在现代GHC中，它等同于RankNTypes，且后者是推荐的扩展名。

下面是底层问题。"这种通用函数的列表"可以具有以下类型：

[forall a. [a] -> [a]]

遗憾的是，这不是一个有效的Haskell类型，因为Haskell不支持“未定多态性”。具体来说，以下程序：

{-# LANGUAGE RankNTypes #-}
myFunctions :: [forall a. [a] -> [a]]
myFunctions = [f1, f2]
   where f1 (x:y:rest) = y:x:rest
         f2 = reverse

会产生以下错误信息：

DebugRank.hs:2:16: error:
    • Illegal polymorphic type: forall a. [a] -> [a]
      GHC doesn't yet support impredicative polymorphism
    • In the type signature: myFunctions :: [forall a. [a] -> [a]]

有一个扩展程序，叫做ImpredicativeTypes。它不稳定而且不完整，但是它允许以下代码编译通过：

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImpredicativeTypes #-}

myFunctions :: [forall a. [a] -> [a]]
myFunctions = [f1, f2]
   where f1 (x:y:rest) = y:x:rest
         f2 = reverse

debug :: [forall a. [a] -> [a]] -> Bool
debug = any combine
  where
    combine :: (forall a. [a] -> [a]) -> Bool
    combine f = usefonBool f && usefonInt f
    usefonBool f = f [True,True] == [False]
    usefonInt  f = f [1,2] == [2,1]

main = print (debug myFunctions)

虽然我不推荐使用它。

通常的替代方案是为多态函数使用newtype包装器：

newtype ListFunction = ListFunction (forall a. [a] -> [a])

这需要一些样板代码，但除了RankNTypes之外不需要任何扩展：

myFunctions :: [ListFunction]
myFunctions = [ListFunction f1, ListFunction f2]
   where f1 (x:y:rest) = y:x:rest
         f2 = reverse

debug :: [ListFunction] -> Bool
debug = any combine
  where
    combine :: ListFunction -> Bool
    combine (ListFunction f) = usefonBool f && usefonInt f
    usefonBool f = f [True,True] == [False]
    usefonInt  f = f [1,2] == [2,1]

完整代码如下：

{-# LANGUAGE RankNTypes #-}

newtype ListFunction = ListFunction (forall a. [a] -> [a])

myFunctions :: [ListFunction]
myFunctions = [ListFunction f1, ListFunction f2]
   where f1 (x:y:rest) = y:x:rest
         f2 = reverse

debug :: [ListFunction] -> Bool
debug = any combine
  where
    combine :: ListFunction -> Bool
    combine (ListFunction f) = usefonBool f && usefonInt f
    usefonBool f = f [True,True] == [False]
    usefonInt  f = f [1,2] == [2,1]

main = print $ debug myFunctions

- K. A. Buhr

---

我真的不明白为什么Rank2Types被弃用了。许多应用程序（包括这个）实际上只需要二阶，没有更高的需求，并且实际上有一个有效的理由可以限制它：二阶多态仍然允许类型推断，而N阶则不行。当然，GHC并没有实现这一点，但它可能会做到。同时，指定Rank2同样有效。另一方面，ImpredicativeTypes应该被弃用——它不能正常工作，从来没有正常工作过，也许在不久的将来也不会。 - leftaroundabout