RankNTypes가 반환 유형

Question

과 일치하지 않습니다. RankNTypes을 사용하여 유형 변수에 의존하지 않는 유형을 정의합니다. 아래 사례를 둘러 보는 것이 올바른 방법입니까?

ST s 안에 사용되는 몇 가지 기능을 정의해야합니다. 물론 s에 의존하지 않습니다. 그러나 이로 인해 두 개의 Int이 적용된 Exp이라는 표현이 Block이되지 않는 문제가 발생합니다. 왜? I로

이

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. 비트입니다까지 : 마지막 라인에 포인트

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] 

내가 오류 : 여기

는 재생기입니다 말할 수있다.

Answer 1

, 나는 대안을 공유하고 싶습니다.

는

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

이유와

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

교체 : impredicative 유형은 (는) 자기 컴파일러는 위의 (.) 및 ($)의 유형을 추측 할 수 있도록.

또 다른 옵션은 (.)과 ($)에 인스턴스화 된 유형으로 주석을 추가하는 것입니다. 그러나 이것은 다소 번거로울 수 있습니다.

Answer 2

Block에 newtype을 사용하면 s을 실용적으로 유지합니다. 그렇지 않으면 밖으로

---

원래 정의를 "누설"을 것이다 : 당신은에 예 (main) 실패 단순화 할 수

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

:

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으로 모든 것이 완벽하게 작동합니다 (012는 필요 없음). 36,) : 나는 @Oleg 게시 솔루션을 선호하는 것 동안

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