search

schell / varying

Continuously varying values, made easy :)
MIT License
40 stars 5 forks source link

VarT violates the applicative laws #5

Closed mitchellwrosen closed 8 years ago

mitchellwrosen commented 8 years ago

I believe the Done constructor was added for efficiency, but exposing the constructor violates the applicative laws.

Consider homomorphism:

pure f <*> pure x = pure (f x)

This is obviously not true since pure (f x) = Done (f x), yet pure f <*> pure x evalutes to some VarT thing.

I've already hand-proven the applicative laws assuming that Done doesn't exist, and instead used pure x = VarT (\_ -> pure (x, pure x)), so the solution (I believe) is either:

  1. Simply hide the VarT constructors
  2. Rewrite <*> to pattern match on Done where appropriate so the laws work out.

Thoughts?

schell commented 8 years ago

It's interesting you brought this up tonight, earlier I removed Done during profiling, I'll check in my changes in a branch and see what you think. For what it's worth though, I think the applicative laws are covered in our test cases. I'll have to check when I'm not on my phone!

schell commented 8 years ago

It looks like we're only testing the applicative laws for splines. I'll have to add a test for regular var streams. 👍

schell commented 8 years ago

@mitchellwrosen - in https://github.com/schell/varying/issues/6 I wrote a test for VarT's applicative homomorphism law. It passes just fine, though that's after I removed the Done constructor, which also greatly improved performance. It's a great win - in my downstream programs I don't even see Control.Varying in profiling any longer!

schell commented 8 years ago

I'm super excited - at least at first glance the changes in #6 allow us to have varying values and the added abstraction of sequencing at a very low cost. Getting rid of the constructors in VarT and changing SplineT's type to use Either instead of a tuple has really improved performance. I think the main problem was that using a tuple (b, Event c) meant that there were many unevaluated output b values kicking around the runtime. The code itself is much less complex using Either, so that is another win.

mitchellwrosen commented 8 years ago

Nice! I just want to clarify that I didn't mean to imply the instance was buggy, but rather it was just incorrect, per the laws. I've seen this pattern before in the operational monad, for example - the main ProgramT type technically violates the monad laws, so its constructors are not exported. Then, end users don't get to see the law violations for themselves.

But, if ripping out the Done constructor actually resulted in better performance, all the better!

mitchellwrosen commented 8 years ago

Oh, did you want me to poke around your pull request too?

schell commented 8 years ago

@mitchellwrosen I always appreciate it. I'm going to merge when Travis finishes clean, but if you look and find anything let me know :)