How to migrate Control.ST code to Idris 2 (Control.App)?

328 views Asked by At

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}?

0

There are 0 answers