Как присвоить значение из монады IO квалифицированному конструктору RankNType

(ОБНОВЛЕНО)

Я создал интерфейс с помощью Free Monad для универсального хранилища данных. Я хочу поместить конкретный интерпретатор (:: DataStore a -> IO a), выбранный пользователем во время выполнения, в монаду состояния вместе с некоторой другой информацией. Кажется, я не могу ничего вставить в это поле в структуре данных.

Как поместить значение в поле, определенное как тип более высокого ранга?

Ниже приведен минимальный пример:

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

Когда я пытаюсь сделать это, GHC жалуется, что:

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
  [...]

ОБНОВЛЕНИЕ

Мой первоначальный минимальный пример был минимальным. Некоторые дальнейшие эксперименты показывают, что проблема возникает, когда мне нужно загрузить интерфейс в монаде IO, чтобы я мог прочитать параметры командной строки. Я обновил пример, чтобы включить эту проблему. Зная это, я могу обойти это кодом.

Интересно, что GHCI сообщает мне, что результаты функции типа IO (DataStore a -> IO a) равны DataStore GHC.Prim.Any -> IO GHC.Prim.Any, чего я не ожидал.


person John F. Miller    schedule 29.07.2016    source источник
comment
Может быть, я упускаю что-то очевидное, но почему бы вам просто не сделать data ProgramState a = PS { ... , storageInterface :: DataStore a -> IO a }? Я не думаю, что это нарушает какой-либо код, который вы вставили сюда...   -  person Alec    schedule 29.07.2016
comment
Не удается воспроизвести проблему.   -  person Alec    schedule 29.07.2016
comment
Алек ` Не в области видимости: переменная типа 'a' `   -  person John F. Miller    schedule 29.07.2016
comment
Вы включили переменную типа data ProgramState **a** = ..?   -  person Alec    schedule 29.07.2016
comment
Нет, я использую RankNTypes. Если бы я этого не сделал, мне нужно было бы экзистенциально определить монаду StateT, в которую она входит, и я просто пнул бы банку по дороге.   -  person John F. Miller    schedule 29.07.2016
comment
Я действительно смущен сейчас. evalState ожидает StateT в качестве первого аргумента, а не ProgramState. Вы имели в виду evalState restOfProgram programState ? На данный момент действительно недостаточно информации, чтобы помочь вам.   -  person Alec    schedule 29.07.2016
comment
Да, я получил аргументы назад. исправлено   -  person John F. Miller    schedule 29.07.2016
comment
Не могли бы вы опубликовать restOfProgram тогда? Это почти наверняка выявит проблему.   -  person Alec    schedule 29.07.2016


Ответы (1)


Проблема здесь в том, что

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

в то время как нам понадобится (непредикативный) тип

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

чтобы код выше работал. Увы, непредикативные типы сейчас в GHC находятся в плачевном состоянии, и их лучше избегать.

Вы можете обойти это, используя оболочку newtype для универсального квантифицированного типа:

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}
  ...
person chi    schedule 29.07.2016