Wie ein RankNType qualifizierter Konstruktor

Question

(AKTUALISIERT)

Ich habe gemacht eine Schnittstelle mit einem Free Monad, um einen generischen Datenspeicher einen Wert aus dem IO Monade asign. Ich möchte den spezifischen Interpreter (:: DataStore a -> IO a), der vom Benutzer zur Laufzeit ausgewählt wurde, zusammen mit einigen anderen Informationen in eine Statusmonade stellen. Ich kann nichts in dieses Feld in der Datenstruktur schreiben.

Wie lege ich einen Wert in ein Feld, das als Typ mit höherem Rang definiert ist?

Im Folgenden finden Sie ein Minimum Beispiel:

{-# LANGUAGE RankNTypes, DeriveFunctor #-} 

data ProgramState = PS { -- line 3 
    [...] 
    , storageInterface :: (forall a. DataStore a -> IO a) 
    } 

data DataStoreF next = 
    Create Asset       (String -> next) 
    | Read  String       (Asset -> next) 
    | Update Asset       (Bool -> next) 
    | UpdateAll [Asset]       (Bool -> next) 
    | [...] 
    deriving Functor 

type DataStore = Free DataStoreF 

runMemory :: (IORef (Map String Asset)) -> DataStore a -> IO a 
runMemory ms (Pure a) = return a 
runMemory ms (Free Create asset next) = [...] 
runMemory ms (Free Read str next) = [...] 
[...] 

pickStorageInterface :: IO (DataStore a -> IO a) 
pickStorageInterface = do 
    opts <- parseOptions 
    case (storage opts) of 
    MemoryStorage -> 
     ms <- readAssetsFromDisk 
     return $ runMemory ms 
    SomeOtherStorage -> [...] 

restOfProgram :: StateT ProgramState IO 
restOfProgram = [...] 

main = do 
    si <- pickStorageInterface 
    let programState = PS { storageInterface = si} -- line 21 
    evalState restOfProgram programState 

Wenn ich versuche, diese GHC zu tun beklagt, dass:

Main.hs: << Line 21 >> 
Couldn't match type `a0' with `a' 
    because type variable `a' would escape its scope 
This (rigid, skolem) type variable is bound by 
    a type expected by the context: DataStore a -> IO a 
    at Main.hs <<line 3>> 
Expected type: DataStore a -> IO a 
    Actual type: DataStore a0 -> IO a0 
In the `storageInterface' field of a record 
    [...] 

---

UPDATE

Mein ursprüngliches minimal Beispiel war minimal. Einige weitere Experimente zeigen, dass das Problem auftritt, wenn ich die Schnittstelle in eine IO-Monade laden muss, damit ich die Befehlszeilenoptionen lesen kann. Ich habe das Beispiel aktualisiert, um dieses Problem zu berücksichtigen. Wenn ich das weiß, kann ich vielleicht damit umgehen.

Interessante GHCI sagt mir, dass die Ergebnisse einer Funktion des Typs IO (DataStore a -> IO a)DataStore GHC.Prim.Any -> IO GHC.Prim.Any ist, was nicht erwartet wurde.

Answer 1

Das Problem hier ist, dass

pickStorageInterface :: forall a. IO (DataStore a -> IO a) 

während wir die (imprädikative) müssten Typ

pickStorageInterface :: IO (forall a. DataStore a -> IO a) 

für den Code oben zu arbeiten. Leider sind die impredikativen Typen jetzt in GHC in einem traurigen Zustand und sollten am besten vermieden werden.

Sie arbeiten rund um kann eine newtype Wrapper um die allquantifizierte Art, dass die Verwendung:

newtype SI = SI { runSI :: forall a. DataStore a -> IO a } 

pickStorageInterface :: IO SI 
pickStorageInterface = do 
    opts <- parseOptions 
    case (storage opts) of 
    MemoryStorage -> 
     ms <- readAssetsFromDisk 
     return $ SI $ runMemory ms 
    ... 

main = do 
    si <- pickStorageInterface 
    let programState = PS { storageInterface = runSI si} 
    ...