なぜこの同等のプログラムはコンパイルされませんか？

Question

このプログラム：

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-} 

import qualified Data.Vector.Mutable as MV 
import qualified Data.Vector as V 
import Control.Monad.ST 
import Control.Monad.Primitive 

unsafeModify :: [(forall s . MV.MVector s Int -> ST s())] -> V.Vector Int -> V.Vector Int 
unsafeModify mods vec = runST $ do 
    mvec <- V.unsafeThaw vec 
    (mods !! 0) mvec 
    V.unsafeFreeze mvec 

コンパイル。このプログラム：

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-} 

import qualified Data.Vector.Mutable as MV 
import qualified Data.Vector as V 
import Control.Monad.ST 
import Control.Monad.Primitive 

unsafeModify :: [(forall s . MV.MVector s Int -> ST s())] -> V.Vector Int -> V.Vector Int 
unsafeModify mods vec = runST $ do 
    mvec <- V.unsafeThaw vec 
    ($ mvec) (mods !! 0) 
    V.unsafeFreeze mvec 

は、次のエラーでコンパイルされません：

Muts.hs:10:15: 
    Couldn't match type ‘forall s1. UV.MVector s1 Int -> ST s1()’ 
        with ‘UV.MVector s Int -> ST s a0’ 
    Expected type: [UV.MVector s Int -> ST s a0] 
     Actual type: [forall s. UV.MVector s Int -> ST s()] 
    Relevant bindings include 
     mvec :: UV.MVector s Int (bound at Muts.hs:9:5) 
    In the first argument of ‘(!!)’, namely ‘mods’ 
    In the first argument of ‘$ mvec’, namely ‘(mods !! 0)’ 

なぜ？

Answer 1

_{注：この投稿はHaskellの文章で書かれています。 Unsafe.lhsとして保存してGHCiで試すことができます。}

---

のは、異なるラインの種類を比較してみましょう：

mods    ::  [(forall s . MV.MVector s Int -> ST s())] 
(mods !! 0)   ::  (forall s . MV.MVector s Int -> ST s()) 
(mods !! 0) mvec ::  forall s. ST s() 


($ mvec)    ::  (MV.Vector s Int -> b) -> b 
     (mods !! 0) ::  (forall s . MV.MVector s Int -> ST s()) 
($ mvec) (mods !! 0) ::  ???????????????????????? 

は、彼らが原因$の型と同等ではありません。

($) :: forall a b. (a -> b) -> a -> b 

あなたが

に沿って何かを必要とするのに対し

($) :: (a ~ (forall s . MV.MVector s Int -> ST s())) => 
     (a -> b) -> a -> b 

は法的ではありません。

しかし、実際にやりたいことを見てみましょう。

> {-# LANGUAGE RankNTypes #-} 

> import qualified Data.Vector.Mutable as MV 
> import qualified Data.Vector as V 
> import Control.Monad.ST 
> import Control.Monad.Primitive 

    unsafeModify :: ??? -> V.Vector Int -> V.Vector Int 

> unsafeModify mods vec = runST $ do 
> mvec <- V.unsafeThaw vec 
> mapM_ ($ mvec) (mods !! 0) 
> V.unsafeFreeze mvec 

物事は原因unsafeModifyの多型の最初の引数modsに厄介です。あなたの元の型

[(forall s . MV.MVector s Int -> ST s())] 

は、それはので、すべての機能は別のsを使用することができ、すべての関数がパラメータs多型である関数の一覧です教えてくれる。しかし、それはあまりにも多くあります。結局のところ

(forall s. [MV.MVector s Int -> ST s()]) 

、我々はそのためsトークンストリームの状態のタイプを同じにすることができ、同じST計算にすべての機能を使用したい：sは、リスト全体throuhgout共有得ればそれは素晴らしいです。私たちは、

> unsafeModify :: (forall s. [MV.MVector s Int -> ST s()]) -> V.Vector Int -> V.Vector Int 

で終わるとsが正しくリスト全体を通してrunSTによって固定されているので、今、あなたのコードは喜んで、関係なく、あなたが($ mvec) (mods !! 0)、(mods !! 0) mvecまたはmapM_を使用するかどうかの、コンパイルされます。悲しいことに

Answer 2

（これはおそらく、コメントする必要がありますが、私はより多くのスペースを必要としています。）

@dfeuerが指摘したように、impredicativeタイプは、GHCで非常にうまく機能しません。 この例を考えてみましょう：

{-# LANGUAGE ImpredicativeTypes, PartialTypeSignatures #-} 
import qualified Data.Vector.Mutable as MV 
import Control.Monad.ST 

-- myIndex :: [forall s. MV.MVector s Int -> ST s()] 
--   -> Int 
--   -> (forall s. MV.MVector s Int -> ST s()) 
myIndex = (!!) :: [forall s. MV.MVector s Int -> ST s()] -> Int -> _ 

による型穴への警告とはいえそれは、正常にコンパイル：

VectorTest.hs:9:69: Warning: 
    Found hole ‘_’ with type: forall s. MV.MVector s Int -> ST s() 
    Relevant bindings include 
     myIndex :: [forall s. MV.MVector s Int -> ST s()] 
       -> Int -> forall s. MV.MVector s Int -> ST s() 
     (bound at VectorTest.hs:9:1) 

我々はPartialTypeSignatures拡張子を削除し、そのタイプforall s. MV.MVector s Int -> ST s()で穴を埋めるために試みることができます。しかし、これは恐ろしく失敗：

VectorTest.hs:9:11: 
    Couldn't match type ‘forall s2. MV.MVector s2 Int -> ST s2()’ 
        with ‘MV.MVector s1 Int -> ST s1()’ 
    Expected type: [forall s. MV.MVector s Int -> ST s()] 
        -> Int -> MV.MVector s1 Int -> ST s1() 
     Actual type: [MV.MVector s1 Int -> ST s1()] 
        -> Int -> MV.MVector s1 Int -> ST s1() 

最後forallは、トップレベルに掲揚、そして今GHCは(!!)の最初の引数はたちの注釈にもかかわらず、単形要素[MV.MVector s1 Int -> ST s1()]のリストでなければならないことを推測します！基本的に、GHCには次の2つの選択肢があります。

-- Note the hoisted forall s1 
myIndex = (!!) :: forall s1. [forall s. MV.MVector s Int -> ST s()] -> Int 
       --^first choice for instantiating the type of (!!) 
       -> MV.MVector s1 Int -> ST s1() 
       --^second choice 

GHCが2番目を選択して失敗します。部分的な型の署名だけで、GHCが正しいことを強いられるように第2の選択肢を削除することができました。

GHCコアのような明示的な型のアプリケーションしかなければ、(!!) @ (forall s. ...)と書くことができましたが、まだありません。