Idris 2 doesn't have Control.ST
, only Control.Monad.ST
which is a completely different beast (it is basically the same as Haskell's Control.Monad.ST
, i.e. mutable references behind a safe, pure interface). It seems that Control.App
is roughly-vaguely what is supposed to replace it. However, the Control.App
documentation isn't written with Control.ST
in mind, and I can't figure out what the migration path is supposed to be.
For example, in this Js frontend library, we have the following 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)]
It is not at all clear what the App
version of this interface would be. Is it supposed to simply use App {l} e ()
everywhere, and the relationship between e
and DomRef {e}
would be tracked somehow differently? Is initBody
/ clearDom
supposed to use the with
pattern, i.e. something like withDom : (App {l} e ()) -> App {l} e ()
? If domPut : {x:a} -> f x -> App {l} e ()
, how is f
's type connected to DomRef {e}
?