在Monad中生成Rank2Type

Question

因此，我表面上理解了Rank2Types，但当我尝试以下内容时

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f :: IO (Process a a)
f = return . auto $ id

GHC咳嗽

Couldn't match type `MachineT m0 (Is a0) a0'
              with `forall (m :: * -> *). Monad m => MachineT m (Is a) a'
Expected type: IO (Process a a)
  Actual type: IO (MachineT m0 (Is a0) a0)
In the expression: return . auto $ id
In an equation for `f': f = return . auto $ id
Failed, modules loaded: none.

因此，据我所见，GHC不允许我在Monad上建立一个框架。这是否有一个原则性的量化逻辑原因，或者这仅仅是GHC的一个限制？还是我只是在做傻事？

Answer 1

您的具体示例如下所示：

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f = (return :: (forall a. Process a a) -> IO (forall a. Process a a)) (auto id)

正如Carl所说，您必须注释您想要非预测地使用的函数，例如此处的return。即使如此，在GHC中使用非谓词类型还是比较脆弱的。我不会推荐的。限制的原因很简单，在非谓词类型存在的情况下执行类型推断是很棘手的，此外，Haskell的表层语言没有适当的语法来指定要实例化多态函数的类型。

一个常见的解决方法是将内容打包到一个newtype中。

data PolyProcess = PP (forall a. Process a a)

f' :: IO PolyProcess
f' = return $ PP $ auto $ id