RankNTypes 与返回类型不匹配

Question

使用RankNTypes，我定义了一个不依赖于类型变量的类型。这是解决以下案例的正确方法吗？

我需要定义一些在ST s 中使用的函数，当然，这些函数并不依赖于s。然而，这会导致一个问题，即应用了两个Ints 的Exp 表达式不会导致Block。为什么？

这是一个复制器：

import Control.Monad.ST
import Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as U
import Data.Vector.Unboxed.Mutable (STVector)
import qualified Data.Vector.Unboxed.Mutable as UM

type Exp = Int -> Int -> Block
type Block = forall s . STVector s Int -> ST s Int

block :: [Block] -> Block
block [] _ = return 0  -- mapM doesn't work, either - ok, I kinda see why
block (e:es) a = do x <- e a
                    xs <- block es a
                    return $ x+xs

copy :: Exp
copy i j a = do
        aj <- a `UM.unsafeRead` j
        UM.unsafeWrite a i aj
        return 1


f :: Block -> Vector Int -> Int
f blk ua = runST $ U.thaw ua >>= blk

g :: Block -> Int
g blk = f blk $ U.fromListN 12 [1..]

main = print . g $ block [copy 10 1]

我在最后一行得到点的错误：

Couldn't match type `STVector s0 Int -> ST s0 Int'
              with `forall s. STVector s Int -> ST s Int'
Expected type: Block
  Actual type: STVector s0 Int -> ST s0 Int
In the return type of a call of `block'
Probable cause: `block' is applied to too few arguments
In the second argument of `($)', namely `block [copy 10 1]'
In the expression: print . g $ block [copy 10 1]

据我所知，预期类型和实际类型之间的区别在于 forall s. 位。

Answer 1

虽然我更喜欢 @Oleg 发布的解决方案，但我想分享一个替代方案。

替换

main = print . g $ block [copy 10 1]

与

main = print (g (block [copy 10 1]))

原因：含意类型使编译器难以猜测上述(.) 和($) 的类型。

另一种选择是使用它们的实例化类型来注释 (.) 和 ($) -- 不过这会相当麻烦。

Answer 2

将newtype 用于Block 将保持s 存在。否则它会“泄漏”出来

---

原定义：

type Block = forall s . STVector s Int -> ST s Int
type Exp = Int -> Int -> Block

您可以将失败的示例 (main) 简化为：

g . block

你希望它的类型是：

g . block :: [Block] -> Int

但是由于组件的写出类型是：

block :: forall s. [forall s0. STVector s0 Int -> ST s0 Int] -> (STVector s Int -> ST s Int)
g :: (forall s1. STVector s1 Int -> ST s1 Int) -> Int

然后当与(.) 组合时，GHC 保持s 通用：

g . block :: forall s . [forall s0. STVector s0 Int -> ST s0 Int] -> Int

并试图统一：

forall s1. STVector s1 Int -> ST s1 Int -- and
(STVector s Int -> ST s Int)

---

newtype 一切正常（不需要ImpredicativeTypes）：

{-# LANGUAGE RankNTypes #-}
import Control.Monad.ST
import Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as U
import Data.Vector.Unboxed.Mutable (STVector)
import qualified Data.Vector.Unboxed.Mutable as UM

type Exp = Int -> Int -> Block
newtype Block = Block { unBlock :: forall s . STVector s Int -> ST s Int }

block :: [Block] -> Block
block [] = Block $ \_ -> return 0  -- mapM doesn't work, either - ok, I kinda see why
block (e:es) = Block $ \a -> do x <- unBlock e a
                                xs <- unBlock (block es) a
                                return $ x + xs

copy :: Exp
copy i j = Block $ \a -> do
        aj <- a `UM.unsafeRead` j
        UM.unsafeWrite a i aj
        return 1


f :: Block -> Vector Int -> Int
f (Block blk) ua = runST $ U.thaw ua >>= blk

g :: Block -> Int
g blk = f blk $ U.fromListN 12 [1..]

main = print . g $ block [copy 10 1]