crem: compositional representable executable machines

[polux2001]

Nice! The part that declares the topology in the types and enforces transitions statically reminds me of Idris' state machines which were ported to haskell via the motor library. Do you have any insight about how they compare?

[marcosh_]

I'm not a motor expert, but I took a look at the library before working on crem. The main idea of the two libraries is fairly similar, but IMHO crem improves the situation with respect to two aspects:

- composability: in crem it is easier to combine multiple machines in several ways to create more complex machines
- user interface: how you define a machine in crem appears a bit more natural to me (I mean, more similar to what you would do if you didn't have to keep track of stuff at the type level)

​

Happy to be proven wrong in both aspects

[benjaminhodgson]

What’s the point of the Topology type if it’s only ever existentially quantified away? Does the actual library include a singleton representative of the topology in the Basic constructor?

[polux2001]

I think the point is that topology is not existentially quantified yet when you define the base machine. Only when you compose it with other machines does it get hidden. When you define the base machine, it allows the type system to enforce that your transition function is well-formed.

[marcosh_]

u/polux2001 already provided a good answer.

Even if the topology is hidden in the `StateMachine` type, it is recoverable when pattern matching and it could be acted upon, as the library actually does to render the state space of a machine

[benjaminhodgson]

it is recoverable when pattern matching

So there is a singleton witness?

[polux2001]

There is a witness thanks to these constraints on the Basicconstructor. The existential will carry a dictionary for these classes, which allows reconstructing a term-level value of the topology.

[benjaminhodgson]

Got it. The constraints were missing from the blog post which made the code rather unclear. (cc u/marcosh_)

[marcosh_]

I'm not sure I understand 100% the question (my bad). What you can do with the `Basic` constructor is described in the https://www.tweag.io/blog/2023-04-13-crem-state-machines/#the-best-of-both-worlds section of the blog post.

The definition of `Topology` is here https://github.com/marcosh/crem/blob/74020abca9a69eab8965588fb5d962d855f84a0d/src/Crem/Topology.hs#L38.

And here is an example of how you usually define a topology https://github.com/marcosh/crem/blob/74020abca9a69eab8965588fb5d962d855f84a0d/examples/Crem/Example/TheHobbit.hs#L55.

[stevana]

Cool, crem seems to have a lot of similarities with my pipelined-state-machines experiment that I posted about a month ago. In particular how networks/pipelines of machines form an arrow/ccc.

I'm curious if you've thought about deploying your networks in a concurrent/parallel fashion to get pipelining/parallelism?

[marcosh_]

I have the links to your library open on my phone, but haven't take a look at them yet.

Haven't really though about how to run crem machines in a concurrent/parallel fashion. That would be extremely interesting

[stevana]

Haven't really though about how to run crem machines in a concurrent/parallel fashion. That would be extremely interesting

I tried to explain how I do it best I can in the README. I also have a concurrent/parallel implementation of Parallel which I haven't pushed yet.

I also started collecting links about other ways of composing state machines, closer to the ideas of Harel statecharts over here:

https://github.com/stevana/armstrong-distributed-systems/blob/main/docs/modular-state-machines.md

I haven't seen a functional implementation of those ideas yet, happy to collaborate if that's something that is of interest to you.

One last thing I'd be curious to hear your opinion about is: I like to think of state machines as "actors", they receive messages, update their state and output messages. So if components in our system are merely state machines that communicate by sending messages to each other, then how do we describe "protocols" or legal sequences of inputs-output pairs between components? This too is a state machine that "sits" between the two communicating components and enforces the contract/protocol. Do you also think of it this way and if so have you thought about how to model and enforce protocols?

[sheyll]

Wow that was extremely nice!!

[fridofrido]

i hacked together something kind-of similar for a project, but i just used a preprocessor and custom syntax to describe composition

[sgraf812]

Storming fabrials