如何解决如何将 Control.ST 代码迁移到 Idris 2 (Control.App)?
Idris 2 没有 Control.ST
,只有 Control.Monad.ST
,这是一个完全不同的野兽(它与 Haskell 的 Control.Monad.ST
基本相同,即安全、纯接口背后的可变引用)。似乎 Control.App
大致是应该取代它的东西。但是,Control.App
文档并没有考虑到 Control.ST
,我无法弄清楚迁移路径应该是什么。
例如,在 this Js frontend library 中,我们有以下 Idris 1 API:
public export
interface Dom (m : Type -> Type) where
DomRef : (a:Type) -> (f : a -> Type) -> (g : a -> Type) -> a -> Type
initBody : List (DomOption a f g) -> ((x:a) -> f x -> Html (g x)) -> (z:a) -> f z -> ST m Var [add (DomRef a f g z)]
clearDom : (dom : Var) -> ST m () [remove dom (DomRef a f g z)]
domPut : (dom : Var) -> {x:a} -> f x -> ST m () [dom ::: (DomRef a f g x)]
目前还不清楚这个界面的 App
版本是什么。是否应该简单地在任何地方使用 App {l} e ()
,并且 e
和 DomRef {e}
之间的关系将以某种方式进行跟踪? initBody
/ clearDom
是否应该使用 with
模式,即像 withDom : (App {l} e ()) -> App {l} e ()
这样的东西?如果 domPut : {x:a} -> f x -> App {l} e ()
,f
的类型如何连接到 DomRef {e}
?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。