如何将IO monad中的值赋给RankNType限定的构造函数 [英] How to asign a value from the IO monad to a RankNType qualified constructor

问题描述

（更新）

我使用免费Monad 到通用数据存储。我想将运行时用户选择的特定解释器（:: DataStore a - > IO a）与其他一些信息一起放入状态monad中。我似乎无法将任何东西放入数据结构的这个字段中。

如何将一个值放入定义为较高排名类型的字段中？

$
$ b

  { - ＃LANGUAGE RankNTypes，DeriveFunctor＃ - } 
 
 data ProgramState = PS { -  line 3 
 [...] 
，storageInterface ::（全部a。DataStore a  - > IO a）
 } 
 
 data DataStoreF next = 
 Create Asset（String  - > next）
 |读取字符串（资产 - >下一个）
 |更新资产（Bool  - >下一个）
 | UpdateAll [Asset]（Bool  - >下一个）
 | 
派生函子
 
类型DataStore = Free DataStoreF 
 
 runMemory ::（IORef（Map String Asset）） - > DataStore a  - > IO a 
 runMemory ms（Pure a）=返回一个
 runMemory ms（下一个自由创建资源）= [...] 
 runMemory ms（Free Read str next）= [... ] 
 [...] 
 
 pickStorageInterface :: IO（DataStore a  - > IO a）
 pickStorageInterface = do 
 opts<  -  parseOptions 
案例（存储选择）
 MemoryStorage  - > 
 ms<  -  readAssetsFromDisk 
 return $ runMemory ms 
 SomeOtherStorage  - > [...] 
 
 restOfProgram :: StateT ProgramState IO 
 restOfProgram = [...] 
 
 main = do 
 si < -  pickStorageInterface 
 let programState = PS {storageInterface = si}  - 第21行
 evalState restOfProgram programState 
  

  Main.hs：<<<第21行>>> 
由于类型变量`a'会跳过它的作用域
，所以`a'
不能匹配`a0'类型
这个（rigid，skolem）类型变量被
a类型绑定上下文预期：DataStore a  - > Main.hs处的IO a 
<<第3行>> 
预期类型：DataStore a  - > IO a 
实际类型：DataStore a0  - > IO a0 
在记录的'storageInterface'字段中
 [...] 
  

更新 我最初的最小例子是最小的。一些进一步的实验表明，当我需要在IO monad中加载接口时出现问题，所以我可以阅读命令行选项。我已更新示例以包含该问题。

有趣的GHCI告诉我，类型为 IO的函数的结果（DataStore a - > ; IO a）是 DataStore GHC.Prim.Any - > IO GHC.Prim.Any 这不是我所期望的。

解决方案

这里的问题是

  pickStorageInterface :: forall a。 IO（DataStore a  - > IO a）
  

我们需要（impredicative） p>

  pickStorageInterface :: IO（所有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（存储选项）
 MemoryStorage  - > 
 ms<  -  readAssetsFromDisk 
 return $ SI $ runMemory ms 
 ... 
 
 main = do 
 si<  -  pickStorageInterface 
让programState = PS {storageInterface = runSI si} 
 ... 
  

(UPDATED)

I have made an interface using a Free Monad to a generic data store. I want to place the specific interpreter (:: DataStore a -> IO a) chosen by the user at run time into a state monad along with some other information. I cannot seem to put anything into this field in the data structure.

How do I put a value into a field defined as a higher rank type?

Below is a minimum example:

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

When I try to do this GHC complains that:

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

My original minimal example was to minimal. Some further experimentation shows that the problem arises when I need to load the interface in an the IO monad so I can read the command line options. I've updated the example to include that issue. Knowing this I may be able to code around it.

Interesting GHCI tells me that the results of a function of type IO (DataStore a -> IO a) is DataStore GHC.Prim.Any -> IO GHC.Prim.Any which is not what I expected.

解决方案

The issue here is that

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

while we would need the (impredicative) type

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

for the code above to work. Alas, the impredicative types are in a sad state now in GHC, and are best to be avoided.

You can work around that using a newtype wrapper around the universally quantified type:

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}
  ...

这篇关于如何将IO monad中的值赋给RankNType限定的构造函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！