Dlaczego ten równoważny program nie jest kompilowany?

Question

Ten program:

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

Kompiluje. Ten program:

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

nie kompiluje się z powodu następującego błędu:

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

Dlaczego?

Answer 1

_{Uwaga: ten post został napisany w literackim Haskell. Możesz zapisać go jako Unsafe.lhs i wypróbować w swoim GHCi.}

---

Porównajmy rodzaje różnych liniach:

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

Oni nie są równoważne z powodu $ „s Typ:

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

O ile będzie trzeba coś wzdłuż

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

co nie jest legalne.

Zobaczmy jednak, co naprawdę chcemy zrobić.

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

Zrobiło bałagan spowodowany unsafeModify jest polimorficzny pierwszy argument mods. Oryginalny typ

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

mówi nam, że jest to lista funkcji, gdzie każda funkcja jest polimorficzny parametr s, więc każda funkcja mógłby użyć innego s. To jednak za dużo. Jest w porządku, jeśli s zostanie udostępniony throuhgout całej listy:

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

Po tym wszystkim, chcemy korzystać ze wszystkich funkcji w tym samym ST obliczeń, dlatego rodzaj stanu strumienia żeton s mogą być takie same. Skończymy z

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

A teraz szczęśliwie kompiluje kod, niezależnie od tego, czy używasz ($ mvec) (mods !! 0), (mods !! 0) mvec lub mapM_, ponieważ s jest teraz prawidłowo ustalone przez runST w całej listy.

Answer 2

(Powinno to prawdopodobnie komentarz, ale potrzebuję więcej miejsca).

Niestety impredicative typy nie działają bardzo dobrze w GHC, jak @dfeuer zauważył. Rozważmy następujący przykład:

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

To kompiluje pomyślnie, aczkolwiek z ostrzeżeniem ze względu na dziury typu:

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) 

Mogliśmy spróbować usunąć rozszerzenie PartialTypeSignatures i wypełnić dziurę z tego typu forall s. MV.MVector s Int -> ST s(). Ale to się nie powiedzie strasznie:

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

Ostatni forall zostanie podniesiona do najwyższego poziomu, a teraz GHC wnioskuje, że pierwszy argument (!!) musi a będzie wykaz elementów monomorficznych [MV.MVector s1 Int -> ST s1()]mimo naszej adnotacji! Zasadniczo GHC ma dwie możliwości:

-- 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 wybiera drugą i kończy się niepowodzeniem. Tylko z częściowym podpisem typu udało mi się usunąć drugi wybór, tak aby GHC został zmuszony do właściwego postępowania.

Gdybyśmy tylko mieli jawną aplikację typu, jak w GHC Core, moglibyśmy napisać (!!) @ (forall s. ...), ale niestety nie mamy.