Tag Archives: frp

Beliefs and the Unimpossibility of Functional Reactive Programming

Behaviors must be first class — this is a belief I have held for almost my entire tenure as an FRP researcher. The belief originated about two weeks after I learned of FRP, when I wrote my first FRP Arrow and in it tried to write a small game. The process was awkward; not as clean and natural as what I had dreamt of for the paradigm. The awkwardness arose when trying to wrangle a time-varying list of time-varying enemies. I concluded that Arrowized FRP (AFRP) was terrible at managing dynamic collections of behaviors, and therefore that an FRP system needed dynamic collections to be powerful enough to do nontrivial things.

Only half of my conclusion was justified. AFRP is indeed terrible at managing dynamic collections of behaviors. But I never questioned the latter half. It epitomizes what Conal Elliott calls “proof by lack of imagination”: since I couldn’t devise a way to write my game without dynamic collections, there must not be a way.

Conal and the rest of the FRP gang has been discussing the semantic junk in classic FRP. Clearly there is more (or rather, less) to an interactive Behavior than an arbitrary function between two non-interactive ones. This identified, my mind immediately jumped to Arrows. That is what they are for: function-like things that can’t do quite as much as regular functions.

And for some reason — perhaps it is my increased functional maturity — I feel no need for first-class behaviors anymore, no awkwardness for their lack. Programming with them doesn’t feel like the rest of functional programming. It feels too open-ended; i.e. I can say too much in the code without saying it in the type. I feel now like Arrows are a perfect fit for FRP. And fortunately, we already have an efficient AFRP implementation. It’s not a great implementation — there are semantic and operational details that could be improved, but it is something to start from, which is more than I had before.

I don’t blame myself for temporarily believing that we needed first-class behaviors. But I am disappointed in myself for taking so long to question that belief. FRP was my world. I was determined to understand it and to make it a practical alternative to Haskell’s IO. But I ended up blatantly ignoring half of the ongoing research because I didn’t believe it would work. This is not acceptable for a serious researcher.

The perfect way is only difficult for those who pick and choose.
Do not like, do not dislike; all will then be clear.
Make a hairbreadth difference, and Heaven and Earth are set apart.
If you want the truth to stand clearly before you, never be for or against.
The struggle between for and against is the mind’s worst disease.
— Zen master Sent-ts’an

Reflections on a Holy Grail (FRP)

It has been two years, twenty-six days, six hours, twenty-four minutes and thirty seconds since my eyes caught the first glimpse of my mistress, functional reactive programming. Her simplicity, beauty, and power has captivated me since, but she has teased me — all of us lonely fools, really — by slipping through my fingers every time, just as I thought I was getting to know her.

A year ago I swore off the cold bitch. She was transforming my life into a single, unhealthy obsession. I needed time to think. Time — there she is again. Maybe by giving myself space, I thought, I could stumble upon a packet of wisdom and finally capture her heart, without really looking for it. But that sort of distance is a lie, my life continues to be about her. Distance only makes the heart grow fonder.

Last week I bumped into her at work. I am not proud of what I did. Forgive me for I am only human, ultimately incapable of suppressing the basal instinct that has ruled my kind for millions of years. That’s right, I implemented her, in the back seat of my Scala convertible. It would seem but a few hour fling on a whiteboard and an editor for the unprivy, but O how it intoxicated me! And it has not, as yet, ended in the heartbreak I have felt over and over again — she is quietly sitting in the back of my codebase, hardly a hundred lines, even doing some good if you can believe it. Maybe I am just fooling myself and this time will be no different. But, at the very least, I feel like I may have learned something.


Perhaps FRP is not the sparkling Holy Grail of interactive functional programming that we have made it out to be. Maybe we cannot find an efficient, general implementation because there is none. Perhaps what we currently know about FRP is what there is to know — a book of heuristics, a collection of experiences and wisdom that tells us which of its features will and will not work together. FRP is not a single feature, you know, it really is a rather large design space, and quite a lot can be done with only pieces of it.

What I did at work was remarkably effective: I sketched how our server would read in FRP language on a whiteboard, and then I implemented a framework which supported exactly the operations I needed and no more. It took hardly two hours, and there is no spacetime leak, no GC nondeterminism. The situation in FRP seems to be something like that of modern theoretical physics: we have a few different theories that all work remarkably well for different kinds of problems, and if only they would work with each other, we would have a unified theory. But mysteriously, they just don’t seem to get along.

A unified theory is more than just something to please the eyes of pure functionalists — it is important to us because it would mean the fall of the IO monad regime. The book of heuristics I claim is FRP still needs a sin bin from which to retrieve the superglue that holds together the pieces of a complete application. So the school of semanticists cannot give a meaning to a complete program, only pieces of it. This makes us unable to prove things about a program, and unsure how to meaningfully compose multiple programs (eg. what kinds of things should and should not be allowed).

There are the quantum field theorists, attempting to bring gravity in to the regime of quantum mechanics; there are the string theorists, attempting to bring the rest of reality into the regime of general relativity. But I, as a physics layman, naively believe that neither of these approaches will end up being the workhorse of the eventual unified theory. I believe that said theory will come with a new way of looking at the world, rather than patching up the old ways. Maybe the expert in me can learn from the layman in me and try to solve the problem instead of clinging to the solution I think I desire.

What is the meaning of an interactive program?

Emphasizing Specialization

I have briefly—or perhaps not so briefly, my interests being unpredictable beasts—shifted the focus of my research to lazy specialization. This topic was discussed extensively, but not comprehensively, in Michael Jonathan Thyer’s dissertation, Lazy Specialization, and seems to have received little attention otherwise. This is unfortunate. I consider it a very important topic.

Lazy specialization is the idea that a functional program be incrementally optimized during its execution, in tandem with partial application. For example, consider the code:

    let g = f x in (g y, g y')

A lazy specializer would evaluate g as far as it could using only information about x, and then apply the resulting optimized function to y and y’.

If most of f’s work could be done using x alone, you could save a lot of time this way. That is the obvious appeal. The drawback on the other side is that the evaluation machinery of a lazy specializer is more involved than a whnf evaluator, so the whole system takes a speed hit as a result.

But so far as I can tell, the only such machines in existence are in a high-level, symbolic, proof-of-concept form, in which the hit is several orders of magnitude. Where’s the research getting down and dirty with this technology, seeing if we can bring it within a factor of 10 or less? Let me argue why we would want to pursue this seriously:

Here is a quote by Heinrich Apfelmus on laziness, at the end of his article on lazy sorting:

Well, it’s highly unlikely that algorithms get faster by introducing laziness. I mean, lazy evaluation means to evaluate only those things that are really needed and any good algorithm will be formulated in a way such that the unnecessary things have already been stripped off. But laziness allows to simplify and compose algorithms. Sometimes, seemingly different algorithms turn out to be two sides of the same coin when formulated with lazy evaluation. Isn’t it great that finding the k-th minimum is not only an adaption of quicksort but can readily be obtained from it by composing it with (!! k)?

I’d say that data structures are the sink for most of the creativity of lazy functional programmers. We spend lots of energy getting a data structure to represent exactly the things we need, sharing what needs to be shared. The key point about data structures is that they can be decomposed; you can peel off the root of a tree and leave yourself with only one of the branches, and the other branch will be garbage collected.

A lazy specializer promotes full-blown functions to the level of data structures. Functions can now be decomposed (by composing!) in the same way, sharing important pieces and forgetting unimportant ones. Observe this stream implementation:

    type Stream a = Nat -> a
    cons x xs z = case z of { Zero -> x; Succ z' -> xs z' }
    tail s z = s (Succ z)

Where Nat is the standard lazy natural type (constructors Zero and Succ). What happens when we evaluate tail (cons 1 (cons 2 R)), for some stream R (I don’t want to bother creating an infinite stream). I’ll use the HNF strategy that I discussed previously. Let’s watch:

   tail (cons 1 (cons 2 R))
   (\s z. s (z+1)) (cons 1 (cons 2 R))
   (\z. cons 1 (cons 2 R) (Succ z))
   (\z. (\z'. case z' of { Zero -> 1; Succ z' -> cons 2 R z' }) (Succ z))
   (\z. case Succ z of { Zero -> 1; Succ z' -> cons 2 R z' })
   (\z. cons 2 R z)

Where did the 1 go? Gone, collected by the garbage collector, just as if we had written Stream in the more conventional way. GHC would have held on to the 1 forever. Nat -> a behaves exactly like the Stream data structure. The structure of Nat has induced a structure for Nat -> a. That is a beautiful form of data structure composability.

Working in a language that uses a lazy specializer also comes with a very important mental advantage: abstracting a pattern using a higher-order function always has constant-time overhead. I.e. you will never make your program run faster by unfolding abstractions. This encourages the more composable higher-order style, providing a snappy comeback to any speed nazi. It also removes the encouragement to fiddle with the details of a function for more speed: beta-equivalent formulations will all turn into the same code in the end, so clarity is the only remaining variable, and can be maximized.

Ideas like GHC’s {-# RULES #-} are no longer fickle compiler constructions, but can now be made trustworthy optimizations. If the left side of a rule is in a certain form (a restricted sort of normal form), then its evaluation can be baked into the interpreter and will be applied as aggressively as possible. It is invariant to fiddling around with higher-order presentations and whatnot; they will be folded away and the rule can be seen. (But I’m not convinced RULES are necessary anymore; perhaps you can simply express the rules you want as a functional construction?)

The most convincing property of lazy specializers to me was the primary bench test for Thyer’s dissertation: the “tower of interpreters” test. This is the property that, if you write an interpreter for a language L, and in language L write an interpreter for M, and in M write an interpreter for N, etc., all the layers will be squashed away and you will end up with code that runs just as fast as it did in the base language (with a constant time overhead for eliminating the layers). You can design a language with all the bells and whistles you want, give it a semantics, and you may immediately use without a significant penalty. This is a huge abstraction win.

But there are a fair number of open problems in lazy specialization, more than just getting faster specialization machines. The explosion problem is tricky, in which, say, fix gradually becomes specialized to things like \f. f (f (f (f (f (f (f (fix f))))))); not useful, just eats up memory. The leap from complete laziness to optimal evaluation needs to be understood better. But in particular, I think we need a real LS to program with for a while, just to see what its dynamics are and to bring out its real-world problems.

I leave you with an addendum (which I snipped from the main argument), explaining my perceived connection between LS and FRP, my personal holy grail. All of my research links back to FRP somehow:

Finally, as if you didn’t know this was coming, there is a connection between lazy specializers and FRP, the holy grail of my functional programming life. It is a particular manifestation of the first point I made, designing streams as functions. I figure, all I have to do is design a data structure for time, with the right domain structure, perhaps something like:

   data Time = Zero | Next Double Time

And then define our friends:

   type Behavior a = Time -> a
   type Future a = (Time, a)

The implementation types exactly equal to their desired semantics, the most beautiful implementation I could ask for. Evaluation for a behavior b has a structure like:

   sample0 = b Zero
   b1 = b . Next 0.033
   sample1 = b1 Zero
   b2 = b1 . Next 0.033
   sample2 = b2 Zero

Each successive b is optimized, the unneeded bits at the front thrown off just as in the Stream example. The reason this can’t be encoded in regular Haskell is because the algebra for FRP includes a value of type Future (Behavior a), and we can’t see inside the Future because it is a functor, and thus arbitrary functions separate us from the enclosed Behavior, about which we must selectively forget things. However, the lazy specializer has no trouble looking through those functions, and will modify the behavior anyway, ridding us of the dreaded space leak.

My Premonition

Last summer I got the opportunity to work briefly with Conal Elliott in Belgium. The two weeks I spent there are still making an impact on me; immediately I resonated with his semantic design idea. But the more important ideas were the ones I picked up subconsciously, and I’m just now becoming able to put them in words.

(1) If extreme idealism isn’t working out for you, maybe it is because you are not wholeheartedly following your own ideals.

(2) You must be the change you wish to see in the world (– Mahatma Gandhi). As applied to software: design software as if it were the beautiful paradise you want it to be, then build pieces of the scaffolding back to the status quo.

Both of these were key insights leading me to undertake Dana.

At the time I was desperately trying to create an FRP framework for Haskell, trying in terms of IO and STM and playing messy tricks with the operational semantics of thunks. It felt like cheating. I had the desire to throw away IO altogether in my efforts, just to see where that led me (this forced me to put aside the way I thought an FRP interface should look). This was an instance of (1).

But in Haskell, IO would always be beneath it all. Your functional program always becomes an imperative program at the end of the day. Maybe this dissonance is what is causing the endless FRP difficulties. Maybe we can’t really know what pure FRP is until we have pure turtles all the way down — until there is no impedance mismatch between the functional and the imperative. This set me on researching the idea of a purely functional operating system, which is still the slogan by which I name Dana.

But now Dana is more than that. Now, it is my (2). In this post, I describe how I see the world of software in 30 years. This isn’t about what kind of devices computers will be embedded in or how they are connected; this is about the process of developing software.

Code and program are the same; any fragment of code may be used interactively. Complex programs are just compositions of simpler ones, and composition of programs is a fundamental concept to both users and programmers. Thus power users cannot help but to be programmers.

Computer science has become a strict subfield of applied mathematics. Creating complex software is primarily modeling: the fundamental task in software development is to create a mathematical model of your problem. The model is encoded directly, and then software scaffolding is built around it, verified to the model. Reasonable shops do not dare ship code that hasn’t been verified to correspond to their model.

Development tools — programs that talk about programs — are astoundingly rich and expressive. Simply enter a property about your code. The tool goes off on a model search to try to refute the property. Meanwhile, in a way that my mind cannot yet comprehend, the programmer communicates the “essence” of why the property should be true, and the tool fills in all the details of the proof. The property is added to a database of facts, which everyone can immediately see and use.

Provably correct code is what people do, because the tools have made it so easy that it is an obvious engineering choice (this ease does not come without a resculpting of our brains). Gargantuan test suites are replaced by a few hours of a developer with a proving tool (an exponential increase in productivity came from the fact that theorems compose, but tests don’t).

User interfaces are mostly an artistic task, quite different from the rigorous visualization that modelers do. All objects have a few obvious ways to endow them with primitive user interfaces (see Eros). Then making a nice user interface is a matter of rearranging them, composing inputs and outputs, and drawing/animating things (under the assumption that computers are still monitor, keyboard, and mouse driven — make the appropriate generalizations).

The shops that will be renowned by power users are those who have a great program with a great interface, but they also ship components to the underlying logic. This is trivial for them, because of the ubiquitous separation between interface and logic. Some are still irrationally afraid of giving away their trade secrets by exposing this, so there are still lame, interface-only programs. But these lame programs will not have the chance to participate in the miracles of engineering the decade will bring, a combiatorical build up of the the work of millions of developers, coming together to create the Star Trek computer — or something else, far more advanced.

Computation is an information science, and is subject to the exponential explosion that comes with it. This Utopian vision hinges on correct composition of everything, from programs to facts.

Right now, software is primarily non-compositional. We have libraries and languages, which are built up of smaller libraries and languages. But end products are not designed to be composed; they are mostly designed for the end user only. But the end user is where the money is, thus where a great deal of the effort in the industry is going. Moreover, for advanced programs (say, Maya), the end user is also where a lot of the skill and talent is.

We have to work at this. There is little small-scale economic incentive to make your program composable; you just give your competitors the ability to use your software without you being able to use theirs. And it’s hard for idealistic young CEOs to try such a thing, since the state of software development means you have to put in a lot of work both to make your program composable and to compose other people’s programs. But these things are not fundamentally hard, they are just hard using the languages and methods of today.

Dana is my own first step in this direction. It aims to be an environment which forces everything to be composable and verifiable. This comes at the expense of mental laziness: you will have to seriously rewire your brain to work in it. I don’t believe that the enlightenment can come without this rewiring. I’m desperately trying to rewire my own, to even consider the choices that will be obvious to the generation ahead.

Is your brain going to be ready when the revolution comes?

Might as well face it, I’m addicted to logic

I’m trying really hard not to become a logician. Like my obsession with FRP, it would be very interesting and educational. But my FRP fancy came from a desire to make games more easily, and I have since lost interest in that endeavor, studying FRP for its own sake. Now I am trying to change the world with Dana, and getting caught up in the beauty and unity of different logical systems.

This happened when trying to choose a core calculus for Dana. I am now furiously interested in Martin Bunder’s work on combinatory logic (btw, if anybody has a copy of his PhD thesis, “a one axiom set theory based on combinatory logic”, please let me know). System IΞ — or rather, systems nearby it — strike me as amazingly beautiful. It is based on an untyped lambda calculus, in which you can prove things about untyped functions (which is a way of endowing them with types). For example, to say that f has type A → B, you say:

Ξ A (B ∘ f)

In English: for all x in A, f x is in B.

However, the core logic really isn’t that important; I’ve only been focusing on it because it’s interesting. In fact, a cool thing about Dana is that there is very little dependency between its parts. But I would really like to start making something rather than researching. How come math is so fascinating?

Anyway, I am not sure that IΞ is strong enough. Assuming a “big enough” universe, I’ve been able to construct an equality predicate (the construction is essentially “the smallest reflexive relation”). But I have had little success in constructing any inductive types, such as the naturals. That’s why I want to read Bunder’s thesis — to get ideas.

Not just system IΞ, but logic in general, is fascinating me. Large cardinals in set theory, universe levels in CIC, and related “stratification” ideas abound and unify to create some intuitive notion of truth. In some sense, truth is the strongest consistent such unverse — however there is provably no such thing. In what system should we then work? Is it essential that picking a system of axioms in which to work will always be a part of mathematics? How do you consolidate results which assume different axioms?

That is actually my current goal for Dana’s core. I think the core calculus will be very weak, and you add axioms as you need more (in line with a quote from Dr. Scott himself: “If you want more you have to assume more”). Such axioms will have the same pattern as e.g. the IO monad in Haskell; your assumptions bubble their way to the top. However, it’s a much richer system than “IO or not IO”; you know exactly what you are assuming to run any piece of code. If there is a top level “user OS”, its assumptions will be vast (or maybe there’s some clever way to incrementally add them?).

Anyway, if the itch to make something irritates me so, I can assume I have a strong core logic — whatever it is — and start building things at a higher level. It’s emotionally difficult for me to do so, because I like to feel like I am on a strong foundation (isn’t that the whole point of Dana, after all?).

Existential Memoization

FRP has this essential trade-off of computation vs. garbage collection. I can come up with implementations which are lazy in their computation, but never forget anything; and I can come up with implementations which forget but are too eager in their implementation (in which garbage collection has too much effect on runtime performance, because we need to kill threads with weak references and stuff). But I can’t come up with an implementation which has both. And my current theory is — I never thought I’d say this — Haskell isn’t good enough!

This language + RTS extension is still in its early stages, and I’ll have to think and prototype more to hash out the details and verify its feasibility. But since I have decided to embark on the Dana project, I am now comfortable with relying on new language features and runtime to get the job done, which previously has not been an option.

Here’s the motivating example. You have a bunch of behaviors — functions from Time to a — which are defined progressively, i.e. they use earlier results to compute later ones. In the best case, we could model these as plain functions of Time, but of course that is not practical in Haskell. In that case, it is lazy computation that never forgets. My idea is to have enough support so that it can forget.

The reason it is allowed to forget is that Time itself is also progressive; i.e. if you have a reference to a some time t, you cannot get to any earlier times. So when the last reference to a time before t disappears, all behaviors can forget everything before time t.

But that’s not a very good solution by itself (unfortunate, because it can be accomplished in Haskell with weak references). The reason is that a single naughty value that holds on to an early time will ruin it for the rest of the program — no behaviors can forget anything after that time. How do we keep the effects more local. Well, when the garbage collector does its run, instead of marking objects as “alive” or “dead”, it can mark them as “needed after t”. So you might mark an object multiple times, with decreasing times each time you see it.

And of course there is nothing special about time. The extension ought to be general enough to handle “stuff like this”. I haven’t even thought about how to make a garbage collector that does this efficiently.

Alright, enough motivation. Onto the language design. I want to add support for ‘progressive folds’, and memoize them with garbage collection. Say you have this data type:

  data U s where
      Succ :: U s -> U s

This looks inane, right? It is unpopulated. Or is it? We can fold a progressive function over this:

  foldU :: (b -> b) -> b -> exists s. (U s, (U s -> b))

I.e. we can define functions over differences of nodes, i.e. in terms of a starting point (which is kind of what the s type variable denotes).

Also, when a particular value U s disappears, we can purge that entry from the memo table and everything that goes along with it. We also know that references inside the scope of the existential eliminator can’t escape, which will end up giving us the time-like relationships I described.

I’m still thinking about the mathematical foundations of this. I.e. what does such an “unrooted” data type mean? This fold also feels less general than it could be; is it possible to introduce two unrooted functions at the same time, or use different recursion schemes, … etc.

The Third Virtue

Ever since working with the Anygma team, the idea of a purely functional operating system has been stirring in my head: An operating system that stays denotational and composable all the way down to the device drivers. In this world, we have to make no sacrifices like IO to interface with the impure ideas around us. We can still communicate with the outside world by modeling them in a pure way.

Just to be clear: I will not be accepting comments about the feasibility of the idea itself (eg. don’t say “but the idea of an operating system is necessarily stateful” or any of that bull). Comments and criticisms about the approach I describe are more than welcome.

So this has been stirring away. Then at Thursday’s Boulder functional programmers group, somebody mentioned Squeak. I had seen Squeak a long time ago, and was amazed and impressed by the concept. There is no distinction between compile time and runtime, between source code and program. Everything is just objects floating around in the world. And of course this matches perfectly with the purely functional operating system idea.

It sucks to program with text. Programs are not text. Ultimately, programs are their denotation, but we need a representation. I say that representation is abstract syntax. Our program editors output abstract syntax, which the compiler turns into real objects. Text doesn’t have to enter the equation anywhere.

I don’t think this idea fits Haskell’s type system very well. We need something closer to dependent types, because types have to be objects floating around in the world too. So, while I’m at it, I think I’m going to make a pure language — pretty close to, but not exactly Haskell — which is the core abstraction language. Maybe something both expressive and barebones like PiSigma. But I’ll need a real-world language to go on top of that.

Hubris indeed.

So! What’s the large-scale plan? I am going to assume nobody will help me (other than to offer suggestions) in these early stages. This is a Grand Vision (TM), and I doubt anybody but me is going to get excited enough to contribute until it starts coming together at least a little. But I am completely excited, as this is the culmination of an idea that has been developing for years. Oh, and that was at the beginning of the large-scale plan because excitement is the top point in my book — engineering is secondary to motivation.

I don’t really know anything about drivers or hardware or any of that, and this undertaking is already way too huge for me. Therefore, I’m going to go the route of Squeak and implement an image-based sandbox — an OS inside an OS. I’ll start by choosing a core language and making a really slow proof-of-concept interactive text-based interpreter for it. At that point, many options open up, depending on what I’m inspired to do at any moment: improve the language frontend, work on graphical hooks, start work on a faster interpreter or JIT, start designing the FRP essentials, ….

As for the FRP essentials, why do I think they will be more possible in this new concept than in Haskell? Well, I have a sophisticated RTS extension that I think will handle that, which I will blog about riiiight… now! (And there are a few ways to compromise in case that idea doesn’t pan out)

Oh, btw, I’m calling this project Dana, after da man Dana Scott.

Ha! I can’t even get Events right

No wonder FRP has been so difficult. In going back to basics, forgetting about behaviors and just doing Events, I realize that my belief that Events are “the easy part” has been flawed. Neither of the semantics I’ve had in mind are both implementable and appropriate. Or rather, they both are, but neither of them can do as much as I thought they could.

I will leave my previously preferred semantics of Event a = Waiter a = Time -> (Time,a), for annoying practical reasons (it also violates intuition about what an event is).

The reactive semantics of Event, Event a = [(Time,a)], is no good because there is always a least occurrence. This violates relativity and intuition (relativity being an intuitive concept I’ve developed regarding the lack of a “global start time”).

So I’m left with Event a = Set (Time, a), or Set (Time, Set a) to handle multiple occurrences at the same time. I am actually inclined to resort to the former, and require a Monoid instance on a to merge. Anyway: what’s the problem with this one? No temporal operations are allowed on it, because it must be observant. Consider mouseClick :: Event Point, the event of mouse clicks. There may be many mouse clicks before the program started, before we were listening for them. If we then sequence mouseClick with some other event, then we have to know about those earlier mouse clicks to detect it. Also consider everySecond :: Time -> Event (), which occurs every second before and after the given time. There are infinitely many occurrences of this event, and so there are infinitely many simultaneous occurrences of everySecond t >> everySecond t. We can not possibly handle all of them.

I know I didn’t motivate that very well, but hopefully you get the idea. If an Event is a set of occurrences, then we must be able to see all of them, including ones that depend on events that happened when we weren’t watching.

I conclude that Event is not a Monad or even Applicative, and all we have is the following interface:

    data Event a
    instance Functor Event
    instance (Monoid a) => Monoid (Event a)
    filter :: (a -> Bool) -> Event a -> Event a
    withTime :: Event a -> Event (Time,a)

Actually, as far as primitives go, I prefer this to filter:

    partition :: Event (Either a b) -> (Event a, Event b)

But they are definable in terms of each other, so it really doesn’t matter except for efficiency concerns. Look how partition is dual to zip. Isn’t that cool?

But in exchange for meaning and implementability, we have given up much of Event’s usefulness. Note that we can no longer even construct the event of double clicks. That makes sense to me, though, because what if the first of the two occurred before we were watching?

I can think of a bunch of ways to get back bits and pieces of the usefulness — EventParsers and the like — and I’m still experimenting with which will be the most effective.

Ridding ourselves of IO before there is a good replacement

I have been researching FRP for about a year now without finding or discovering an implementation I like. I don’t know if there is one — maybe my standards are just too high. However, it has initiated me into the more general interest of purely functional foundations.

Since I am tired of thinking and want to start hacking again, I am abandoning FRP proper for the time being. But I am continuing in spirit, by continuing with foundations. I will be developing this project in the Frag repository, where I keep my FRP stuff.

The idea of the Frag project is simple: get back to making the software I want to make — mostly games — but shun IO. I.e. the content of these will only be built on semantically meaningful abstractions (which are in turn implemented on IO, of course), but without concern for making it a “perfect” FRP implementation. Said abstractions will go in the Frag project. The main point is to get away from the world of fuzzy, complex operational semantics, replacing it lazily with simple denotational ones.

But this is a foundational project, meaning that once the foundations are replaced, I allow myself to do arbitrary software engineering on top of it. I think this is an important point.

Currently in the repository is a simple Event abstraction. I’m seeing how much I can write with just that, without worrying about modeling conceptually continuous things (like mouse position). Secretly my plan is to accidentally come across a good interaction model which boils down to Event, and is thus inherently meaningful (simplicity can be refined out later).

I’m having trouble foreseeing how I will model eg. network interaction using Events. Graphical games are pretty easy, since conceptually they always exist, and you’re just choosing to view them. I can’t see how network fits into a model like this, since a network program can have side-effects on another computer. Can anyone think of a way that network interactions are about being instead of doing?

Continuous Stream Fusion

I’ve been able to sketch-implement a version of FRP with a strange distinction: Env vs. Behavior. I’ll give you the intuition, then the rest of the article will develop the semantics more fully. I thought “backwards” to discover this (the word “discover” used under the assumption that it has some merit: questionable), from implementation, to concept, to semantics.

The semantics of Env a are plain ol’ Time -> a, but with a caveat: there is no reactivity allowed. I.e. an Env a yields an a only by looking at stuff “now”. In the implementation, this is just a subtype of IO. The semantics of Behavior are even less defined. I guess it’s semantics are Time -> Time -> a, so it is given a “start time” and returns a time function. It’s sortof like a relative behavior, but shifting it around does not exactly preserve behavior. The implementation is much like Reactive (Env a), where Reactive is from the popular reactive library. But through this exploration I am led to a very different implementation.

To formalize this silliness, first we need to add some composability and define these as transformations. Let’s just fix an e for the whole discussion, and then say the meaning of Env a is (a subtype of) (Time -> e) -> (Time -> a). Now it’s easy to say what we mean by not allowing reactivity: an Env a is a function f of the form f r = g . r for some g. So to determine the value of f at time t, you look at its environment at time t and do something to the result. No peeking at other points in its environment.

For Behavior, I want a scanl, but on continuous functions. You can think of this as a generalization of integration. For a continuous scan to be meaningful, I require its argument to be a continuous function f of type Real -> a -> a, such that f 0 = id. By continuity I mean Scott-continuity: treat Real as an infinite-precision computable real, and then any definable total function is continuous.

Then I can find the integral function ∫f on the interval [0,1] by computing the limit:

  f 0.5  .  f 0.5
  f 0.25  .  f 0.25  .  f 0.25  .  f 0.25

There is no guarantee that this will converge, or uniformly converge, or any of that good stuff. But we will cover our ears and pretend that it always does.

If f :: Real -> Bool -> Bool, once our precision goes past the modulus of uniform continuity of f (the precision of the information that f will never look at to determine what to do), then ∫f will be constant. So there is some notion of continuity preserved.1

Okay, now we can say what a Behavior is! The meaning of Behavior a is a transformation f :: (Time -> e) -> Time -> Time -> a of the form — hold your breath (I’ll explain) — f r t0 = i . ∫ (j r) (k (r t0)), for functions i,j,k, where j is an Env function with the scan restriction j 0 = id.

Let’s dissect: First, k (r t0) is the initial value when the Behavior is started, which depends on the environment exactly when the Behavior is started and no other time. j r is the integrand, which takes into account the “previous” value and the current environment (only current because j must be an Env function). Finally, the i . out front is so we can compute things more complex than their final type; i.e. a Behavior Bool could have more state under the hood than just a boolean.

This definition is very much like Haskell stream fusion; we take a recursive definition and “flatten it out” into a state and an iterator function. By imposing a simple constraint on the iterator function, we have retrieved continuity of the generated stream, and can also perform continuous stream fusion in the implementation!

I still haven’t figured out how to work events back into this model.

1 I’m committing a blatant foul here. Bool -> Bool is a discrete space, so any continuous function from Real to it has to be constant to begin with. So that paragraph was pretty much meaningless. I still liked it to get a computational handle on things.