Perché questo programma equivalente non viene compilato?

Question

Questo programma:

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

compila. Questo programma:

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

non si compila con il seguente errore:

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)’ 

Perché?

Answer 1

_{Nota: questo post è scritto in Haskell letterale. Puoi salvarlo come Unsafe.lhs e provarlo nel tuo GHCi.}

---

Mettiamo a confronto i tipi di diverse linee:

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) ::  ???????????????????????? 

Essi non sono equivalenti a causa di $ s' Tipo:

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

Mentre si avrebbe bisogno di qualcosa sulla

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

che non è legale.

Tuttavia, diamo un'occhiata a ciò che effettivamente si vuole fare.

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

le cose sono in disordine a causa di unsafeModify s' polimorfica primo argomento mods. Il tuo tipo

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

originale ci dice che è una lista di funzioni, dove ogni funzione è polimorfica il parametro s, quindi ogni funzione potrebbe utilizzare un altro s. Tuttavia, è troppo. Va bene se il s ottiene condiviso throuhgout la lista completa:

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

Dopo tutto, vogliamo utilizzare tutte le funzioni nella stessa ST calcolo, quindi il tipo di stato del canale di token s può essere lo stesso. Finiamo con

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

E ora il codice compilato felicemente, indipendentemente dal fatto che si utilizza ($ mvec) (mods !! 0), (mods !! 0) mvec o mapM_, perché s è ora fissato correttamente runST in tutta la lista.

Answer 2

(questo dovrebbe probabilmente essere un commento, ma ho bisogno di più spazio.)

Purtroppo, i tipi impredicativa non funzionano molto bene in GHC, come @dfeuer sottolineato. Considerate questo esempio:

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

Compila con successo, anche se con un avvertimento a causa del buco tipo:

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) 

Potremmo cercare di rimuovere l'estensione PartialTypeSignatures e riempire il buco con il suo tipo forall s. MV.MVector s Int -> ST s(). Ma questo non riesce orribilmente:

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() 

L'ultima forall ottiene issata al primo livello, e ora GHC deduce che il primo argomento di (!!) deve essere un elenco di elementi monomorfa [MV.MVector s1 Int -> ST s1()]nonostante nostra annotazione! Fondamentalmente, GHC ha due scelte:

-- 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 sceglie il secondo e non riesce. Solo con una firma di tipo parziale sono stato in grado di rimuovere la seconda scelta in modo che GHC fosse costretto a fare la cosa giusta.

Se solo avessimo un'applicazione di tipo esplicita come in GHC Core, avremmo potuto scrivere (!!) @ (forall s. ...), ma purtroppo non l'abbiamo fatto.