2

Idris 2 没有Control.ST，只Control.Monad.ST​​有它是一个完全不同的野兽（它与 Haskell 的基本相同Control.Monad.ST，即在安全、纯接口后面的可变引用）。似乎Control.App大致模糊地应该替换它。但是，Control.App编写文档时并没有Control.ST考虑到，我无法弄清楚迁移路径应该是什么。

例如，在这个 Js 前端库中，我们有以下 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 ()之间的关系会以不同的方式被跟踪？是否/ 应该使用该模式，即类似的东西？如果，'s type 是如何连接的？eDomRef {e}initBodyclearDomwithwithDom : (App {l} e ()) -> App {l} e ()domPut : {x:a} -> f x -> App {l} e ()fDomRef {e}

4

0 回答 0