如何将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屋!