Monday, July 28, 2014

Homemade FRP: a study in following the types

I wonder how FRP is implemented? Since I only know about a small part of reactive-banana so far, this is the interface I am currently thinking of when I think of FRP:

data Event t a
data Behavior t a

instance Functor (Event t)
instance Functor (Behavior t)
instance Monoid (Event t)
instance Applicative (Behavior t)

filterE :: (a -> Bool) -> Event t a -> Event t a
accumE :: a -> Event t (a -> a) -> Event t a
stepper :: a -> Event t a -> Behavior t a

I have omitted never and union, because they are just mempty and mappend from Monoid. I have also omitted accumB, because my understanding is that accumB x e is just a more efficient version of stepper x (accumE x e), and I am not concerned at all about efficiency yet.

Interactivity


So, how do I implement this interface? Could I represent Event as a map from timestamp to values, for example? It sounds like this representation would admit an implementation for all the required functions, but that would not allow me to handle events as they come, like I can do with gloss-banana. I would have to open the window, and let the user click around without being able to update the display. After accumulating all the mouse events, I would gather them into one big map, an Event t InputEvent, from which I could construct an Event t Picture. At this point, I would know exactly what I should have displayed after each of the mouse clicks, but it would be too late for that. Clearly, I need to find a way to obtain the early outputs before I learn about the later inputs...

With a list instead of a map, I can think of at least two laziness-based approaches for this kind of problem, but I'm not ready for a clever implementation yet. Let's keep things simple!

I said that a map-based representation would not allow me to handle events as they come. So clearly, being able to handle events as they come should be part of my API. What would a function for handling a new event look like?

handleInputEvent :: InputEvent -> Event t a -> IO (Maybe a)

I give the next InputEvent, the Event decides what it wants to do with it, and optionally triggers an event of type a based on it. But it's weird to have such a concrete type as InputEvent; surely reactive-banana isn't aware of the specifics of the event types supported by gloss. Event should have a type parameter indicating which type of input events it expects. Oh! Maybe that's what the t is for?

handleEvent :: t -> Event t a -> IO (Maybe a)

Much better. You might wonder why I am returning an IO action instead of a pure Maybe a: it's because of accumE. Accumulating the values of the events as they come requires storing an intermediate state somewhere, and a pure function would not be able to store its new state anywhere.

Well, I don't want to be stuck inside IO yet, so let's thread this state explicitly:

handleEvent :: t -> Event t a -> (Maybe a, Event t a)

I give the next t-valued input event, the Event decides what it wants to do with it, and optionally triggers an event of type a. The Event might have changed its internal state somehow, so it also returns a modified copy of itself, one which is ready to receive the next event.

Event


I now have a much clearer idea of the way in which I am going to use (or "eliminate", in type-theory-speak) values of type Event, but I'm no closer to figuring out how to represent those Event values. Or am I? When a type has a single (or a most general) eliminator, we can just use that eliminator as a representation:

data Event t a = Event
  { runEvent :: t -> (Maybe a, Event t a)
  } deriving Functor

handleEvent = flip runEvent

Is this representation good enough? Can the rest of the API be implemented on top of it? As I get stuck trying to implement union, I remember that one input event can cause more than one output event to be emitted at the same time. I make a small adjustment:

data Event t a = Event
  { runEvent :: t -> ([a], Event t a)
  } deriving Functor

With this representation, I can easily derive an implementation for the first few combinators, simply by following the types. A good sign!

instance Monoid (Event t a)
  where
    mempty = Event (const ([], mempty))
    e1 `mappend` e2 = Event go
      where
        go t = (xs1 ++ xs2, e1' <> e2')
          where
            (xs1, e1') = runEvent e1 t
            (xs2, e2') = runEvent e2 t

filterE :: (a -> Bool) -> Event t a -> Event t a
filterE p e = Event go
  where
    go t = (filter p xs, filterE p e')
      where
        (xs, e') = runEvent e t

Interlude: on the technique known as "follow the types"


Following the types is a technique which allows a function to be implemented very quickly, by taking decisions based on the types of the values involved instead of their meaning. Since it happens so quickly, it's a process which is a bit difficult to describe, as stopping in the middle of it in order to take notes will break the magic. Here is an attempt at reconstructing the magic after the fact.

First, let's dispel a possible misconception: I'm not a human version of djinn. That is, when I "follow the types", I do not blindly pick a random expression of the expected type, hoping it will be correct. Instead, I use the types as a shortcut when there is only one obvious way to go forward, and otherwise I pick an expression which fits the immediate context.

For example, in the code for filterE, I begin with the Event constructor, I pass it an intermediate function receiving a value of type t, and I eliminate the e argument using its only eliminator and the only value of type t I have on hand. I did not waste any time on those uninteresting details, because there are simply no alternatives to consider.

The call to filter p xs, on the other hand, is deliberate: a simple xs would have had the same type, but would have been incorrect. Yet the reason I used filter was not because I stopped to think about correctness; that would have involved reasoning based on the meaning of the values. Instead, I knew from the start that I wanted to filter out values of type a. It is the context of implementing an event-filtering function which guided me through the non-forced parts of the implementation: as I was following the types, I was on the lookout for values of type a or [a], ready to filter them on sight. This kind of context is also the reason why I used [] in the definition of mempty, versus (++) in the definition of mappend.

A very different example of context is that of the recursive call to filterE p e', where e and e' would have also type-checked. This part of the implementation is in a recursive position for Event t a, just like the tail is a recursive position for lists. In such a recursive context, I naturally picked a recursive expression, of the proper type of course, and using smaller arguments where possible.

Simplification


After a type-based implementation, I like to take a moment to go beyond the types and examine the meaning of all the values involved. Reading the code I just blindly wrote for never/mempty, the Event in which no event ever occurs, I see that the first input event is ignored, and that no output events are produced in response. Afterwards, recursively, no event ever occurs, and that's exactly what I want.

This reviewing phase is also a good opportunity for simplifications, such as replacing (\_ -> ...) with const or rearranging the pieces in a pointfree style. One simplification opportunity I notice is that [] is the mempty for lists, and (mempty, mempty) is the mempty for pairs, and const mempty is the mempty for functions. This, and a similar chain for mappend, allows the Monoid implementation to be simplified greatly:

instance Monoid (Event t a)
  where
    mempty = Event mempty
    Event e1 `mappend` Event e2 = Event (e1 `mappend` e2)

In this version, all the details are implicit, so much so that it's hard to follow the meaning of the values. But it's also a much more elegant implementation, and I've just read and understood the expanded-out version anyway, so I'm confident that the meaning is what I expect.

Behavior


The workflow for Behavior and its combinators is very similar to Event, so let's go through it quickly.

How do I represent/eliminate a Behavior? Probably the same way I eliminate events, except that behaviours have a value at every point in time, so I should receive exactly one a instead of a (potentially-empty) list of them.

data Behavior t a = Behavior
  { runBehavior :: t -> (a, Behavior t a)
  } deriving Functor

Trying to implement stepper, I realize that a behaviour is also supposed to hold a value before the very first event, and also between events. I need a second eliminator:

currentValue :: Behavior t a -> a

Now I have two eliminators. What would be a most general eliminator, from which the two others could be implemented?

generalEliminator :: Behavior t a -> (a, t -> Behavior t a)

I no longer need an a on the right-hand side of the (t -> ...), because currentValue can extract this a from the returned behaviour. I transform this most general eliminator into a representation for Behavior, giving convenient names to the pair's two components:

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: t -> Behavior t a
  } deriving Functor


Following the types is very straightforward this time.

instance Applicative (Behavior t)
  where
    pure x = Behavior x fx
      where
        fx _ = pure x
    Behavior f ff <*> Behavior x fx = Behavior (f x) fy
      where
        fy t = ff t <*> fx t

As before, this can be simplified: (\_ -> x) is the pure x for functions, and thus fx could be written as pure (pure x). Similarly, fy could be written by nesting two (<*>), whatever that means. This hints at a variant implementation of Behavior based on Compose, which will hide the details of the nesting:

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: Compose ((->) t) (Behavior t) a
  } deriving Functor

instance Applicative (Behavior t)
  where
    pure x = Behavior x (pure x)
    Behavior f cf <*> Behavior x cx = Behavior (f x) (cf <*> cx)

I'm not convinced that this variant is actually better, because the other combinators don't benefit from Compose: they just peel off the Compose layer, do their work, and put it back on. Speaking of the other combinators, I've skipped two of them in my exposition. I left them for the end, because...

When following the types leads nowhere


The last two combinators don't fit the mantra of following the types very well. Here is part of accumE:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = (_xs, ...)
      where
        (fs, e') = runEvent e t

The next step is to find an expression of type [a] for _xs. Unused values include fs, of type [a -> a], and x, of type a. One obvious and type-correct way to combine those two values is to apply all the functions in the list to x:

        _xs = fmap ($ x) fs

But we're in an accumulator context, so I'm expecting something like a fold instead. When something doesn't seem right, it's best to stop following the types and switch to "figure out what I'm trying to do" mode.

In this case, what I am trying to do is to thread the x through all the functions, returning all the intermediate values. It turns out there is a standard library function for that, scanl:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = (xs', accumE x' e')
      where
        (fs, e') = runEvent e t
        xs = scanl (flip ($)) x fs
        x' = last xs
        xs' = tail xs  -- skip the initial unmodified x

If I was more familiar with scanl, I could have used it without thinking, remaining in follow-the-types mode. But then I wouldn't have thought to skip scanl's initial copy of x, I might have recurred with x instead of last xs, and everything would have been completely wrong.

My implementation for the last combinator is also quite wrong:

stepper :: a -> Event t a -> Behavior t a
stepper x e = Behavior x (Compose go)
  where
    go t = stepper x e'
      where
        (xs, e') = runEvent e t

I did not use xs, and as a result, I recur on the wrong x. Here is what I should have written instead:

stepper :: a -> Event t a -> Behavior t a
stepper x e = Behavior x (Compose go)
  where
    go t = stepper (last (x:xs)) e'
      where
        (xs, e') = runEvent e t

The only trick here is that I prepend x to xs in order to ensure that the argument to last is non-empty.

Conclusion


Following the types didn't work for every single combinator, but when it did work, it quickly produced a correct implementation on the first attempt.

Yup, it's working!
It even has the same leak-until-clicked behaviour as the original :)

When it didn't work, following the types did not lead to any wasted work. For ease of presentation, I have shown an incorrect type-based version followed by a corrected meaning-based version, but during my original implementation, there wasn't a sharp break between the two phases. Like I said, it all happens very quickly, so it's hard to describe exactly what is going on inside my head when I code. I think I always focus on the correctness of what I write. It's just that over time, I have learned that when the types which are in scope are sufficiently distinct, it's okay for "correct" to mean simply "type-correct". Whereas at other times, perhaps mere seconds later, it becomes important to understand what the values actually mean.

If you came here to learn how to follow the types yourself, and you're disappointed by my vague explanations, don't be. I did not set out to learn to follow the types; I just wrote lots of Haskell code, and my brain learned to focus on the types when appropriate. You'll get there, don't worry.

No comments: