Test algebraic laws of primitives using Quickcheck

[milibopp]

Test algebraic laws of primitives using Quickcheck

[milibopp]

Let's start to specify the semantics that ought to be tested here. Much of this is taken/adapted from Conal Elliott's paper on Push-Pull FRP. We assume a testable notion of equality denoted as ==. Furthermore, trait bounds like Send + Sync + Clone + 'static are implied as required and omitted for better readability.

Streams

Monoid

For reference: Wikipedia: Monoid

The streams of type Stream<T> should form a monoid under Stream::merge with Stream::never() being the identity. Thus, for arbitrary a, b, c: Stream<T> the following properties hold:

• left identity: Stream::never().merge(&a) == a,
• right identity: a.merge(&Stream::never()) == a,
• associativity: a.merge(&b).merge(&c) == a.merge(&b.merge(&c)).

While this certainly holds when all events are fired in separate transactions, there could be an issue with events from the same transaction.

Functor

For reference: Wikipedia: Functor (type theory)

Streams form a functor under Stream::map, i.e.

• the identity function is preserved: a.map(|x| x) == a,
• it respects function composition: a.map(f).map(g) == a.map(|x| g(f(x))).

Here, f: Fn(T) -> U and g: Fn(U) -> V if a: T.

Monad

For reference: Wikipedia: Monad (functional programming)

Streams in principle form a monad under a bind or flat_map operation defined as:

fn bind<T, U, F: Fn(T) -> Stream<U>>(a: &Stream<T>, f: F) -> Stream<U> {
    a.map(f).switch()
}

(Question: Push-Pull FRP delays past event occurrences until the generation of the inner event. Is this necessary for the algebraic laws to hold? And how does this compare to the non-lazy transactional environment Carboxyl's working in?)

The neutral element is less trivial to construct in Carboxyl. In Push-Pull FRP it is modelled as a stream that fires exactly once in the infinite past. We cannot do this. However, maybe it is possible to mimick it somehow like this:

fn return<T>(value: T) -> Stream<T> {
    let sink = Sink::new();
    let stream = sink.stream();
    sink.send(value); // Too early?
    stream
}

(We can't call it return because that's a keyword in Rust, but I wanted to use Haskell terms as a reference.)

The problem here is obviously, that the value will be sent before any consumers of the stream can listen to it. Somehow streams must be constructed in such a way, that return(x).hold(y) always samples as x. This may require some tweaks to the internals. (E.g. an event could hypothetically store its last occurence as an optional value.)

Nonetheless, for adequate implementations of return and bind the monad laws state that

• return acts as a neutral element:
  • return(x).bind(f) == f(x),
  • a.bind(return) == a,
• a.bind(f).bind(g) == a.bind(|x| f(x).bind(g).

The monad implies an applicative functor but this is not a particularly useful notion here (see Elliott paper).

Signals

Functor

Signals form a functor under unary lifts. So for a: Signal<T>, f: Fn(T) -> U, g: Fn(U) -> V

• lift!(|x| x, &a) == a,
• lift!(|x| g(f(x)), &a) == lift!(g, &lift!(f, &a)).

Applicative functor

For reference: Haskell docs on Applicative

To make signals an applicative we need a pure function, which in Carboxyl's API is the same as Signal::new, creating a signal with a constant value. Further we need a combining operator like this:

fn cmb<A, B, F: Fn(A) -> B>(f: &Signal<F>, a: &Signal<A>) -> Signal<B> {
    lift!(|f, a| f(a), f, a)
}

Note: A (small) technical problem here is that most functions in Rust are not Clone. This could be alleviated by wrapping it in an Arc. However, in the long-term this should be addressed by an upstream RFC, as this work-around introduces a performance penalty. For simplicity, we'll assume that closures are Clone here.

Now, the following laws must hold:

• identity: cmb(&pure(|x| x), &a) == a
• composition: cmb(&cmb(&cmb(&pure(comp), &f), &g), &h) == cmb(&f, &cmb(&g, &h)) where f, g, h are signals of composable functions and comp denotes function composition.
• homomorphism: cmb(&pure(f), &pure(x)) == pure(f(x))
• interchange: cmb(&f, &pure(x)) == cmb(&pure(|g| g(x)), &f)

Monad

Elliott mentions that signals also form a monad, but does not elaborate this. Presumably this works with similarly to streams using switch to construct the bind operation. Constructing return should be easier as it is simply Signal::new. This monad may imply the applicative above.