函数组合和 forall'ed 类型

假设我们有一些这样的代码，其类型检查效果很好：

{-# LANGUAGE RankNTypes #-}

data Foo a

type A a = forall m. Monad m => Foo a -> m ()
type PA a = forall m. Monad m => Foo a -> m ()
type PPFA a = forall m. Monad m => Foo a -> m ()

_pfa :: PPFA a -> PA a
_pfa = _pfa

_pa :: PA a -> A a
_pa = _pa

_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

main :: IO ()
main = putStrLn "yay"

我们注意到_pp x = _pa $ _pfa x太冗长了，我们尝试将其替换为_pp = _pa . _pfa。突然，代码不再进行类型检查，失败并显示类似于以下内容的错误消息

• Couldn't match type ‘Foo a0 -> m0 ()’ with ‘PA a’
  Expected type: (Foo a0 -> m0 ()) -> Foo a -> m ()
    Actual type: PA a -> A a

我想这是由于m在类型别名的定义中foralld — 事实上，替换m使用某些确切的类型可以解决问题。但问题是：为什么forall在这种情况下会破坏东西吗？

尝试找出为什么替换虚拟递归定义的奖励积分_pfa and _pa与平常一样_pfa = undefined结果 GHC 抱怨统一变量和命令多态性：

• Cannot instantiate unification variable ‘a0’
  with a type involving foralls: PPFA a -> Foo a -> m ()
    GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
  In an equation for ‘_pfa’: _pfa = undefined

只是为了清楚起见，当你写下：

_pa :: PA a -> A a

编译器扩展类型同义词，然后向上移动量词和约束，如下所示：

_pa
  :: forall a.
     (forall m1. Monad m1 => Foo a -> m1 ())
  -> (forall m2. Monad m2 => Foo a -> m2 ())

_pa
  :: forall m2 a. (Monad m2)
  => (forall m1. Monad m1 => Foo a -> m1 ())
  -> Foo a -> m2 ()

So _pa具有 2 级多态类型，因为它有一个嵌套在函数箭头左侧的 forall。同样适用于_pfa。他们期望多态函数作为参数。

为了回答实际问题，我首先向您展示一些奇怪的东西。这些都进行类型检查：

_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

_pp :: PPFA a -> A a
_pp x = _pa (_pfa x)

然而，这并没有：

apply :: (a -> b) -> a -> b
apply f x = f x

_pp :: PPFA a -> A a
_pp x = apply _pa (_pfa x)

不直观，对吧？这是因为应用程序运营商($)在编译器中是特殊情况，允许使用多态类型实例化其类型变量，以支持runST $ do { … }而不是runST (do { … }).

作品(.)然而，并不是特例。所以当你打电话时(.) on _pa and _pfa，它首先实例化它们的类型。因此你最终试图通过非多态性的结果_pfa，类型(Foo a0 -> m0 ()) -> Foo a -> m ()错误消息中提到的函数_pa，但它需要一个类型的多态参数P a，所以你会得到一个统一错误。

undefined :: a不进行类型检查，因为它尝试实例化a具有多态类型，是谓述多态性的一个实例。这是关于你应该做什么的提示——隐藏必然性的标准方法是使用newtype包装：

newtype A a = A { unA :: forall m. Monad m => Foo a -> m () }
newtype PA a = PA { unPA :: forall m. Monad m => Foo a -> m () }
newtype PPFA a = PPFA { unPPFA :: forall m. Monad m => Foo a -> m () }

现在这个定义编译没有错误：

_pp :: PPFA a -> A a
_pp = _pa . _pfa

您需要显式包装和展开以告诉 GHC 何时抽象和实例化的成本：

_pa :: PA a -> A a
_pa x = A (unPA x)