6

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

{-# 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
4

2 回答 2

6

只是要清楚，当你写：

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

rank-2 多态类型也是如此_pa，因为它有一个嵌套在函数箭头左侧的 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 { … }).

但是，组合(.)不是特殊情况。所以当你调用and(.)时，它首先实例化它们的类型。因此，您最终尝试将错误消息中提到的类型的非多态结果传递给函数，但它需要一个类型的多态参数，因此您会收到统一错误。_pa_pfa_pfa(Foo a0 -> m0 ()) -> Foo a -> m ()_paP 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)
于 2017-05-13T05:38:27.593 回答
2

用多态类型实例化多态类型变量称为隐含多态。-- GHC 用户指南

如错误消息所示，GHC 仅允许使用单态、等级 0 类型来实例化类型变量。我的猜测是，使用隐含多态性进行类型检查比看起来更难实现。

于 2017-05-12T20:57:55.500 回答