3 ms·
Lately I've been experimenting with comonads to structure stateful code. The idea is that a comonad describes the interface for a state machine, and you can con
by danharaj 10y ago
Lately I've been experimenting with comonads to structure stateful code. The idea is that a comonad describes the interface for a state machine, and you can convert any comonad in Haskell into a monad transformer which acts as a restricted form of the state monad. The state monad describes expressions that can arbitrarily manipulate a state of some type. The monad you derive from a comonad does not have direct access to its state, the comonad describes all the allowed manipulations and queries.
This is all described and implemented here: https://hackage.haskell.org/package/kan-extensions-5.0.1/docs/Control-Monad-Co.html https://hackage.haskell.org/package/kan-extensions-5.0.1/doc...
In particular, the type:
data CoT w m a = CoT { runCoT :: forall r. w (a -> m r) -> m r }
Let's unpack this. The following type represents a state machine whose nodes are labeled with a continuation demanding an `a` and executing an effect:
w (a -> m r)
The forall quantification in CoT means that it does not care what the result value is. It will take a state machine, manipulate it for a bit, produce an `a`, pick a continuation from the state machine and execute it.
That's a lot going on! I don't have time or space to explain how this is actually useful but here's a handy approximation:
- `w` is an interface
- `w s` is a model labeled with a value of `s` for each state it can occupy. These labels are a sort of view.
- `CoT w m a` is a controller that can manipulate a model and compute in some effectful context.
High powered MVC. The upshot is that because we're leaning on Functors, Monads, and Comonads there are extremely well behaved and natural composition operations. For example, `fmap` allows us to change the view of a model by applying a pure function. The fact that `CoT` is a monad means that we can run controllers in serial, as well as combine our controller languages in sensible ways. The fact that `w` is a comonad means we can reason about the behavior of models equationally. This lets us transform, compose, and compare models with mathematical precision.
This is a project I only seldom work on in my spare time. I have already applied it to writing GUI's and game logic to good effect but I'm still exploring the design space regarding reactivity and temporal behavior. This has led me to reading the mathematical literature pertaining to products of comonads/sums of monads (they're dual).