如何将 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 (将#修改为@）