haskell - 在 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 中添加 forall 。这是否有一个原则性的、量化的逻辑原因，或者这只是 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