功能组成和forall'ed类型

Question

假设我们有一些像这样的代码,哪些类型很好:

{-# 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类型别名的定义是forall'd - 确实,用m一些确切的类型替换修复了这个问题.但问题是:为什么forall在这种情况下会破坏事物？

试图弄清楚为什么用GHC中的通常结果替换虚拟递归定义的原因_pfa,抱怨统一变量和不可预测的多态性:_pa_pfa = undefined

• 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

Answer 1

只是要清楚,当你写:

_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 ()

所以_pa有一个rank-2多态类型,因为它有一个嵌套在函数箭头左边的forall.同样如此_pfa.他们期望多态函数作为参数.

要回答实际问题,我首先会向您展示一些奇怪的东西.这些都是typecheck:

_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 { … }).

(.)然而,组合物不是特殊的.所以,当你打电话(.)的_pa和_pfa,它首先实例化它们的类型.因此,您最终尝试将错误消息中提到的类型的非多态结果传递给函数,但它期望类型的多态参数,因此您会得到统一错误._pfa(Foo a0 -> m0 ()) -> Foo a -> m ()_paP a

undefined :: a没有进行a类型检查,因为它试图用多态类型实例化,这是一种impregicative多态的实例.这是一个关于你应该做什么的暗示 - 隐藏impredicativity的标准方法是使用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)