Почему эта эквивалентная программа не компилируется?

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

Они не эквивалентны из-за $ «s типа:

($) :: 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 «s полиморфного первого аргумента mods. Ваш тип оригинала

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

говорит нам, что это список функций, где каждая функция является полиморфным параметр s, поэтому каждая функция может использовать другой s. Однако это слишком много. Это нормально, если s получает общий throuhgout всего списка:

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

В конце концов, мы хотим, чтобы использовать все функции в одном ST вычислений, поэтому типа состояния потока маркеров s могут быть одинаковыми. Мы в конечном итоге с

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

И теперь ваш код счастливо компилирует, независимо от того, используете ли вы ($ mvec) (mods !! 0), (mods !! 0) mvec или mapM_, потому что s теперь корректно фиксируется runST по всему списку.

Answer 2

(Это, вероятно, следует комментарий, но мне нужно больше пространства.)

К сожалению, непредикативные типы не очень хорошо работает в GHC, так как @dfeuer указал. Рассмотрим следующий пример:

{-# 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 имеет два варианта:

-- 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 выбирает второй и не работает. Только с неполной подписью типа я смог удалить второй вариант, чтобы GHC был вынужден делать правильные вещи.

Если бы у нас было явное приложение типа, например, в GHC Core, мы могли бы написать (!!) @ (forall s. ...), но, увы, мы этого не сделали.