Korzystanie z jednowartościowy szeregowych typu 2

Question

Oto kod:

{-# LANGUAGE RankNTypes, FlexibleContexts, ScopedTypeVariables #-} 

module Foo where 

import Data.Vector.Generic.Mutable as M 
import Data.Vector.Generic as V 
import Control.Monad.ST 
import Control.Monad.Primitive 
import Control.Monad 

data DimFun v s r = 
    DimFun {dim::Int, func :: v (PrimState s) r -> s()} 

runFun :: (Vector v r) => 
    (forall s . (PrimMonad s) => DimFun (Mutable v) s r) -> v r -> v r 
runFun t x = runST $ do 
    y <- thaw x 
    evalFun t y 
    unsafeFreeze y 

evalFun :: (PrimMonad s, MVector v r) => DimFun v s r -> v (PrimState s) r -> s() 
evalFun (DimFun dim f) y | dim == M.length y = f y 

fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r) 
fm = error "" 

f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r) 
f = liftM runFun $ (fm :: forall s . (PrimMonad s) => m (DimFun (Mutable v) s r)) 

Wynika to z błędów:

Couldn't match type ‘DimFun (Mutable v) s0 r’ 
       with ‘forall (s :: * -> *). PrimMonad s => DimFun (Mutable v) s r’ 
Expected type: DimFun (Mutable v) s0 r -> v r -> v r 
    Actual type: (forall (s :: * -> *). 
       PrimMonad s => 
       DimFun (Mutable v) s r) 
       -> v r -> v r 
Relevant bindings include 
    f :: m (v r -> v r) (bound at Testing/Foo.hs:36:1) 
In the first argument of ‘liftM’, namely ‘runFun’ 
In the expression: liftM runFun 

Jednak nie jestem pewien, jak to naprawić lub zdiagnozować problem. Może to być tak proste, jak dobrze (i dobrze napisany) podpis typu.

Starając się zrozumieć, co się dzieje, piszę wersję non-jednowartościowy (bezużyteczny dla mnie), ale kompiluje:

gm :: (MVector v r, PrimMonad s, Num r) => DimFun v s r 
gm = error "" 

g :: forall v r m . (Vector v r, Num r) => v r -> v r 
g = runFun (gm :: forall s . (PrimMonad s) => DimFun (Mutable v) s r) 

To czyni mnie rzeczą błąd powyżej jest związane z this question tam, gdzie nie ma miejsca na słownik, ale to po prostu ukłucie w ciemności.

Answer 1

Jednym z rozwiązań jest przeniesienie ograniczenia PrimMonad w typ danych DimFun.

data DimFun v r = DimFun 
    { dim :: Int 
    , func :: forall s . PrimMonad s => v (PrimState s) r -> s() 
    } 

Reszta kodu kompiluje jak jest usunięcie parametru s z DimFun:

runFun :: Vector v r => DimFun (Mutable v) r -> v r -> v r 
runFun = ... 

evalFun :: (PrimMonad s, MVector v r) => DimFun v r -> v (PrimState s) r -> s() 
evalFun = ... 

fm :: (MVector v r, Num r, Monad m) => m (DimFun v r) 
fm = ... 

f :: (Vector v r, Num r, Monad m) => m (v r -> v r) 
f = liftM runFun fm 

Przesuwanie ograniczenia klasy do typu danych może wydawać się przerażające dla ciebie, ale w rzeczywistości, to już w każdym razie miał tam przymus klasy. PrimState jest typem skojarzonej rodziny PrimMonad, więc aby wyprodukować lub zużyć v (PrimState s) r, potrzebujesz ograniczenia PrimMonad.

Jeśli jednak chcesz tego uniknąć, będziesz musiał zmienić typ czegoś. Aby zrozumieć, dlaczego funkcja masz jest illtyped, należy rozważyć następujące kwestie (które wymaga ImpredictiveTypes):

fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r) 
fm = error "" 

g :: (Vector v r, Monad m) 
    => m (forall s . PrimMonad s => DimFun (Mutable v) s r) -> m (v r -> v r) 
g = liftM runFun 

Należy wyczyszczone dlaczego g fm jest illtyped: g oczekuje czegoś gdzie forall s . PrimMonad s => jest wewnątrzm, który jest nie w przypadku fm. Będziesz musiał napisać funkcję typu:

fm' :: (MVector v r, Monad m, Num r) => m (forall s . PrimMonad s => DimFun v s r) 
fm' = error "" 

f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r) 
f = g fm'