Grammars for articulating effects, for state machines with strongly typed transitions

[pygy]

Hi, I'm not familiar with the literature, and my naive searches lead to nothing so far. This may not be a new idea, if it's been experimented with I'd love get pointers. This may also be off base...

A natural extension of typed effects would be to let users articulate grammars. E.G. for file operations, with a RegExp-like syntax, Open(Read|Write)*Close would prevent one from writing to a file that hasn't been opened yet (I know there are better ways to enforce this, this is for the sake of the example).

This would enable one to ensure at compile time that a piece of code respects a given protocol (e.g. that you can't write HTTP headers while the body is being sent).

[matijapretnar]

This sounds to me like session types, though those are mostly used for describing protocols between communicating clients. For a connection with effect systems, you could start with D. Orchard & N. Yoshida: Effects as sessions, sessions as effects.

[pygy]

Thanks @matijapretnar this is exactly what I was after (and then some).