Join behaviour

[larrytheliquid]

Finally got some more time to read over the runtime :)

I had to fix an insertBefore argument order bug for this to also work for upstream DOMNodeBehaviour's.

There were a few other unrelated bugs I spotted, but it's better to turn those fixes into separate commits.

P.S. I think the infrastructure you've built around the agda js backend and this project is very promising, thanks!

[asajeffrey]

Finally back from PoPL... I had a look over your patch, but I'm a bit concerned that it's overspecialized to the case ⟦ Beh (Beh (DOM w)) ⇒ Beh (DOM w) ⟧, in particular the code for attachTo which has been duplicated. Really this is an instance of a bigger disease, which is that my code assumes that for any node n of type Beh (DOM w), that n.value == n. You can see this all over the place in the code, e.g. in:

ConcatBehaviour.prototype.notify = function(now,value) {
    this.length = this.downstream1.length + this.downstream2.length;

the assumption is that this.downstream1 is a DOMNodesBehaviour, and so has a length field.

The invariant that the only nodes of type Beh (DOM w) are instances of DOMNodesBehaviour is broken by the introduction of join, since we can now have nodes of type Beh (DOM w) which are instances of JoinBehaviour instead.

There are a couple of possible fixes here:

a) Make JoinBehaviour a delegate for every method that a behaviour node might export, or

b) Rewrite the rest of the codebase to be more careful about the distinction between nodes of type Beh (DOM w) and DOMNodeBehaviours.

I am tempted by (b) since JS doesn't really support delegating, but it does introduce quite a bit of inefficiency, e.g.

ConcatBehaviour.prototype.notify = function(now,value) {
    this.length = this.downstream1.value.length + this.downstream2.value.length;

[asajeffrey]

PS: I should say thanks for your thanks :-)

[larrytheliquid]

Oh yeah strange, some of the existing methods already do delegate to value (like ConcatBehaviour.prototype.appendChildrenOf) and some don't.

I think option b) sounds good as well (hopefully the inefficiency won't be too terrible, since it's just a constant time hash lookup).

I've just started to work on some rudimentary tests for FRP Behaviour stuffs (there are too many combinations of things now to just rely on the demos). Hopefully that will make changes like these a little less worrisome.

[asajeffrey]

OK, so the invariant we're maintaining is that any node whose Agda type
is "Beh (DOM w) s" should have a value field which is an instance of
DOMNodesBehaviour. I think that should be maintainable.

Some tests for FRP behaviours sounds excellent, especially if they can
be run in the same way as the existing unit tests (which test the
non-FRP behaviours). A DOM mocking library would probably be helpful here.

A.

On 01/30/2012 06:03 PM, Larry Diehl wrote:

Oh yeah strange, some of the existing methods already do delegate to value (like ConcatBehaviour.prototype.appendChildrenOf) and some don't.

I think option b) sounds good as well (hopefully the inefficiency won't be too terrible, since it's just a constant time hash lookup).

I've just started to work on some rudimentary tests for FRP Behaviour stuffs (there are too many combinations of things now to just rely on the demos). Hopefully that will make changes like these a little less worrisome.

---

Reply to this email directly or view it on GitHub:
#3 (comment)

[larrytheliquid]

Made change and added tests for Behaviour and DOM, let me know what you think.

[asajeffrey]

I'll try to have a look at this and get back to you tomorrow.

On 02/02/2012 07:20 PM, Larry Diehl wrote:

Made change and added tests for Behaviour and DOM, let me know what you think.

---

Reply to this email directly or view it on GitHub:
#3 (comment)

[asajeffrey]

OK, this is mostly looking pretty cool. The only thing I'm not sure about is the compareAs method, and its use in the test suite via equalNow. Are compareAs and equalNow just used for testing purposes, or are they needed for something else?

[larrytheliquid]

Yeah, they are just used for testing.
I'm not sure what kind of equality API is eventually desirable on the Agda side of things. For example we might want bisimilarity, or perhaps something like equalNow but have it require a predicate for its polymorphic parameter (though that would mean requiring a polymorphic predicate for DOM outside of Beh which I haven't thought about and might be weird).

My line of thinking was that only exposing equalNow/compareAs in the tests via ≟ seemed like an adequate compromise to get Behaviour/DOM testing achieved (and tackling some kind of equality being exposed in the library another day).

[asajeffrey]

I think I'd rather do this by making QUnit.agda FRP-aware rather than
adding code that's only needed for testing into the FRP runtime. The
question is what its semantics should be, perhaps something like (using
ASCII representations of some Unicode):

ok<> : [[ Beh < Bool > ]] -> Test

where ok<> b is considered to be passing if at some time it has value
true (hence the diamond in its name).

There's probably some nasty behaviour with timeouts we'd need to impose
here, such that failing tests get reported after some period of time,
which would involve digging back into the qunit code, which I currently
only vaguely remember :-)

A.

On 02/03/2012 12:15 PM, Larry Diehl wrote:

Yeah, they are just used for testing.
I'm not sure what kind of equality API is eventually desirable on the Agda side of things. For example we might want bisimilarity, or perhaps something like equalNow but have it require a predicate for its polymorphic parameter (though that would mean requiring a polymorphic predicate for DOM outside of Beh which I haven't thought about and might be weird).

My line of thinking was that only exposing equalNow/compareAs in the tests via ≟ seemed like an adequate compromise to get Behaviour/DOM testing achieved (and tackling some kind of equality being exposed in the library another day).

---

Reply to this email directly or view it on GitHub:
#3 (comment)

[larrytheliquid]

Hm, yeah having a temporal eventually-like test would also be useful to tests effects from events that eventually happen (though what is currently there suffices for behaviours + dom).

I'm not sure if you would be able to keep the logic outside of signal.js though, as how to compare is specialized to the kind of behaviour:
larrytheliquid/agda-frp-js@master...join#L7R331
larrytheliquid/agda-frp-js@master...join#L7R395
larrytheliquid/agda-frp-js@master...join#L7R454

[asajeffrey]

For the simple tests in FRP.JS.Test.Behaviour we just need a map2 of type:

∀ {A B C} → ⟦ A ⇒ B ⇒ C ⟧ → ⟦ Beh A ⇒ Beh B ⇒ Beh C ⟧

then we can specialize it to:

≟* : ⟦ Beh ⟨ ℕ ⟩ ⇒ Beh ⟨ ℕ ⟩ ⇒ Beh ⟨ Bool ⟩ ⟧
≟* = map2 ≟

The case of DOM nodes is trickier though. I'd like to avoid exposing DOM
node identity, but I'm OK with exposing a structural equality on DOM
nodes, so there'd be a function:

DOMNodesBehaviour.prototype.equals

which could then be wrapped inside a map2 to give an Agda-level function
of type:

≟ : ∀ {w} → ⟦ Beh (DOM w) ⇒ Beh (DOM w) ⇒ Beh ⟨ Bool ⟩ ⟧

This can then be exported as part of the DOM interface, not just in the
Test interface.

A.

On 02/03/2012 02:20 PM, Larry Diehl wrote:

Hm, yeah having a temporal eventually-like test would be nice to also be able to affects from events that eventually happen (though what is currently there suffices for behaviours + dom).

I'm not sure if you would be able to keep the logic outside of signal.js though, as how to compare is specialized to the kind of behaviour:
larrytheliquid/agda-frp-js@master...join#L7R331
larrytheliquid/agda-frp-js@master...join#L7R395
larrytheliquid/agda-frp-js@master...join#L7R454

---

Reply to this email directly or view it on GitHub:
#3 (comment)

[larrytheliquid]

I like the cut of your jib, will try to experiment with this over the weekend.

[larrytheliquid]

Here's a branch with the suggested updates (the commit history would still need to be rebased/rewritten/cleaned):
larrytheliquid/agda-frp-js@master...try-map2

equalsNow is gone in favor of map2 plus the special _≟*_ private instantiation of map2 for DOM Behaviour equality.
This branch is using ok[t] (ok at time t/now) rather than ok◇ (okay at some time in the future), only because I didn't want to deal with implementing the timeout version now.

One thing I still couldn't make my mind up about was where withDOW should belong:
larrytheliquid/agda-frp-js@master...try-map2#L12R12

Currently its just in FRP.JS.Test.DOM. It could be added to QUnit, or even use a separate dom-ok[t] or something, but I was afraid of the combinatory explosion of ok-variations with and without dom.

[asajeffrey]

Some thoughts... Mainly this is looking pretty good.

We should remove attachTo from Map2, and instead be careful about
calling foo.value.bar rather than foo.bar when foo has type (DOM w s).

The .equals method is currently giving an equality based on HTML
serialization, which might do weird things in corner cases (in
particular I'm not sure what it's going to do with attached event
listeners). I'm slightly concerned we'll end up breaking Agda's
referentially transparent semantics.

Can we rename ok[t] to ok◇ and put a comment saying that we should add a
timeout to it at some point in the future?

For withDOW, perhaps the DOW module should export an "unattached" value
of type DOW? This would represent a DOM location that will never be
attached to the main DOM tree.

A.

On 02/04/2012 09:51 PM, Larry Diehl wrote:

Here's a branch with the suggested updates (the commit history would still needs to be rebased/rewritten/cleaned):
larrytheliquid/agda-frp-js@master...try-map2

equalsNow is gone in favor of map2 plus the special _≟*_ private instantiation of map2 for DOM Behaviour equality.
This branch is using ok[t] (ok at time t/now) rather than ok◇ (okay at some time in the future), only because I didn't want to deal with implementing the timeout version now.

One thing I still couldn't make my mind up about was where withDOW should belong:
larrytheliquid/agda-frp-js@master...try-map2#L12R12

Currently its just in FRP.JS.Test.DOM. It could be added to QUnit, or even use a separate dom-ok[t] or something, but I was afraid of the combinatory explosion of ok-variations with and without dom.

---

Reply to this email directly or view it on GitHub:
#3 (comment)

[larrytheliquid]

Can we rename ok[t] to ok◇ and put a comment saying that we should add a
timeout to it at some point in the future?

Done.

For withDOW, perhaps the DOW module should export an "unattached" value
of type DOW? This would represent a DOM location that will never be
attached to the main DOM tree.

Good idea, done.

We should remove attachTo from Map2, and instead be careful about
calling foo.value.bar rather than foo.bar when foo has type (DOM w s).

Map2 does not define attachTo, did you mean Join? Right now it's
necessary so that the joined behaviour won't get GC'd (via the
upstream element). Also notice that the notify in the upstream
actually appends the new DOM behaviour to the node. As the fastclock
demo demonstrates, this is important because you can have a behaviour of
different doms to render over time. The only time this actually occurs
is when a join behaviour is a topmost DOM that will be used as
data-main. It feels kind of kludgy but I'm not sure how to avoid it.

The .equals method is currently giving an equality based on HTML
serialization, which might do weird things in corner cases (in
particular I'm not sure what it's going to do with attached event
listeners). I'm slightly concerned we'll end up breaking Agda's
referentially transparent semantics.

If possible, I would really like to actually compare rendered
html. The primary motivator to add DOM tests was to get test coverage
of the dom rendering code. That being said, I share your concern about
breaking referential transparency with respect to quirks in dom
events. Getting some test coverage of dom events firing would be nice
here.

Another option I was tempted to do was to define a method that
essentially gives you back a json-like representation of the dom tree and
use that in .equals. This would less risky then using the dom, but
once again that would mean losing test coverage of dom rendering.

Thanks for the continued detailed feedback, I think this is coming
along nicely.

larrytheliquid/agda-frp-js@master...try-map2#L12R12

[asajeffrey]

We should remove attachTo from Map2, and instead be careful about
calling foo.value.bar rather than foo.bar when foo has type (DOM w s).

Map2 does not define attachTo, did you mean Join?

Oops, yes I did.

Right now it's
necessary so that the joined behaviour to not get GC'd (via the
upstream element). Also notice that the notify in the upstream
actually appends the new DOM behaviour to the node. As the fastclock
demo demonstrates, this is important because you can have a behaviour of
different doms to render over time. The only time this actually occurs
is when a join behaviour is a topmost DOM that will be used as
data-main. It feels kind of kludgy but I'm not sure how to avoid it.

Oh rats, of course you need to attach the node to stop it being GC'd.
D'oh! Perhaps we should move attachTo into Behavour, so it will then be
inherited by all nodes of type Beh (DOM w) t.

The .equals method is currently giving an equality based on HTML
serialization, which might do weird things in corner cases (in
particular I'm not sure what it's going to do with attached event
listeners). I'm slightly concerned we'll end up breaking Agda's
referentially transparent semantics.

If possible, I would really like to actually compare rendered
html. The primary motivator to add DOM tests was to get test coverage
of the dom rendering code. That being said, I share your concern about
breaking referential transparency with respect to quirks in dom
events. Getting some test coverage of dom events firing would be nice
here.

Fair enough. I think we're safe, that .equals will just compare the HTML
content with the event handlers stripped out. As long as there's an
invariant being maintained that if two Agda expressions are
propositionally equal then their HTML serializations are equal, then I
think we're OK.

Another option I was tempted to do was to define a method that
essentially gives you back a json-like representation of the dom tree and
use that in .equals. This would less risky then using the dom, but
once again that would mean losing test coverage of dom rendering.

Best to stick with the built-in DOM-renderer I think, since HTML is such
a tricky beast.

Thanks for the continued detailed feedback, I think this is coming
along nicely.

Indeed, we're pretty close to the magic moment when I can press the
"merge changes" button, thanks for all the effort you're putting in!

[larrytheliquid]

Cleaned commit history, and shared attachTo code via anchor and initializeChildrenOf.

• DOMNodesBehaviour.attachTo
• Join.attachTo
• Behaviour.anchor
• DOMNodesBehaviour.initializeChildrenOf

[asajeffrey]

Hooray, change merged. Welcome to the project!

[larrytheliquid]

Nice :)