RankNTypes不匹配返回類型

Question

使用RankNTypes，我定義了一個不依賴於類型變量的類型。這是否正確的方式來解決下面的情況？

我需要定義一些在ST s內使用的函數，當然這並不取決於s。然而，這導致了一個問題，即Exp的兩個Int適用於它的表達式不會導致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])) 

原因：impredicative類型使它很難編譯器猜測(.)和($)上述類型。

另一種選擇是使用它們的實例化類型註釋(.)和($) - 但這樣會比較麻煩。

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]