[Agda] Searching for a state machine library

[Marko Dimjašević]

Dear Agda community,

Is anyone aware of an Agda library for finite state machines that has
capabilities like Control.ST in Idris? The Idris library is described
at:

http://docs.idris-lang.org/en/latest/st/state.html

At the link, the library is described like this:

"The Control.ST library provides facilities for creating, reading,
writing and destroying state in Idris functions, and tracking changes
of state in a function’s type. It is based around the concept of
resources, which are, essentially, mutable variables, and a dependent
type, STrans which tracks how those resources change when a function
runs."


The main idea is the STrans type constructor with this signature:

STrans : (m : Type -> Type) ->
         (resultType : Type) ->
         (in_res : Resources) ->
         (out_res : resultType -> Resources) ->
         Type

(This is written in Idris, but I am sure you can easily see how it
would look like in Agda.)

If you know of such a library in Agda, I would appreciate a pointer to
it!


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191023/1115fce7/attachment.sig>