Discarding Disjoin

I lost motivation to keep working on my RDPIO implementation – I got sick of carrying Haskell type constraints around. Not Haskell’s fault, just premature generalization on my part. So I’ve recently started a fresh implementation of RDP, called Sirea (simply reactive) for now. My goal with Sirea is to favor concrete types – one time type, one signal kind, one behavior kind – and keep it simpler. I’ll still use vat concepts under-the-hood, for example, but I won’t be exposing vats directly to users of Sirea – which ultimately means more Haskell threads will be involved to handle periodic IO tasks (such as UI rendering loops).

In the switch, I initially tabled disjoin and constrained dynamic behaviors even further. And then I got to thinking, should I try to include disjoin?

Recall, disjoin will divide a signal in the environment based on a division elsewhere:

bdisjoin :: B (x :&: (y :|: z)) ((x :&: y) :|: (x :&: z))

This is a powerful primitive for RDP. It splits signals in `x` based on the activity of `y` or `z`. It is somewhat analogous to splitting actions on lexical scope across an if/then/else expression, except that’s difficult to do in a reactive context.

But the (:&:) and (:|:) types represent complex, asynchronous or partitioned signals!

Tangent: In RDPIO, I was thinking that partitioning would be part of concrete signal types – i.e. `s x` could indicate partition somewhere in `s`. In Sirea, since I have only one signal type, I represent it as `S p a` where `p` represents the partition. For certain values of p (via Data.Typeable) I might even automatically generate multi-threaded behaviors, which is much more convenient than my old RDPIO approach. (I took that idea from FRP.Sodium.)

Back on topic, one of my goals with RDP is to keep communication costs obvious, by which I mean: communication between partitions should always have an explicit representation in code. I think there is no way to achieve this with disjoin, since masking the `x` signal would require some communication from the `y` and `z` signals.

Weaker Disjoin?

I believe I could still benefit from a weakened variation of disjoin, something like:

bdisjoin_w :: B (S p x :&: (S p y :|: S p z)) (S p (x,y) :|: S p (x,z))

This would essentially distribute the x signal across the y and z signals. The implicit `bzip` behavior is unfortunate, but does accurately reflect the actual implementation of such a behavior. Developers would be able to apply this behavior multiple times if necessary, each time bringing in another set of external values.

This is a bit inconvenient, though. I need something more generic for the y and z types.

Alternative to Disjoin?

A simple alternative to disjoin is to use an intermediate service – writing to it in one branch, reading from it in the other. This technique is elegant in its own way – analogous to if/then/else in imperative systems where the entire lexical environment is represented as state.

bdisjoin_dm :: B (x :&: (y :|: z)) ((x :&: y) :|: (x :&: z))
bdisjoin_dm = bfirst bwrite_x >>> bsnd >>> (bload_dm +++ bload_dm)
   where bload_dm = bcopy >>> bfirst (bdrop >>> bread_x) 

-- given
bread_x :: B (S p ()) x
bwrite_x :: B x x

A problem here is that the demand-monitor might be shared. That’s probably acceptable; developers can apply a little discipline.

If I had linear types, perhaps I could achieve the properties equivalent to the original disjoin only needing an extra argument to provide a source of uniqueness. (I have very mixed feelings about linear types in RDP. Modeling local state is powerful and useful, but it also tends to be unstable to structural changes in code, and difficult to maintain.)

Dynamic Behaviors

As I mentioned earlier, dynamic behaviors have a similar problem. Here is the analog of the definition for eval I presented in the earlier article:

beval :: B x y -> B (S p (B x y) :&: x) y

The idea is that you describe `eval default` and the default behavior is used in case the behavior carried by the signal is illegal (e.g. too much latency). Defaults aren’t essential, they’re just an artifact of Haskell lacking more expressive types. Since writing that earlier article, I’ve come to favor an alternative that simply inlines the error behavior and allows developers to set the latency:

beval :: DT -> B (S p (B x y) :&: x) (y :|: Error)

Both of these have the same problem as disjoin: the `x` type might be split across multiple partitions, which are not `p`, and thus eval would require a lot of implicit communication across partitions to install the behavior.

For Sirea, I think I’ll scale this back to something like:

beval' :: DT -> B (S p (B (S p x) y) :&: S p x) (y :| S p Error)

That is, eval can only accept local parameters. Again, this doesn’t satisfy me. But opening up a remote partition and surgically tweaking where the `x` signals go isn’t exactly trivial communication. Long term, I’d like to see if I can explicitly implement my original concept of eval atop this simplistic variation.

Addendum April 7 2012

I finally found a (weakened) disjoin signature that I’m satisfied with:

bdisjoin :: B (S p a :&: ((S p () :&: x) :|: y) )
              ( (S p a :&: x) :|: (S p a :&: y) )

This splits an external signal (S p a) based on a signal representing the choice in the same partition (S p ()). There is no more `decision at a distance`, since everything is in one partition. This works well with generic signal types (x, y). We only need information from one branch to perform the split (due to RDP’s duration coupling properties). The actual implementation is achieved by masking signals – a simple mask for the left, and a mask with the inverse of the unit signal for the right.

Addendum May 13 2012

I’ve found a way to get a decent amount of generality from disjoin sig in Haskell:

bdisjoin :: (SigInP p x) => B (x :&: ((S p () :&: y) :|: z) )
              ( (x :&: y) :|: (x :&: z) )

The SigInP typeclass requires every component in x be in partition p. (Requires FlexibleInstances.)

This entry was posted in Reactive Demand Programming. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s