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.

2 thoughts on “Existential Memoization

  1. Note: This particular example buys us nothing, and can be implemented in Haskell.

    newtype U s = U { unU :: [s] }
    succ = U . tail . unU
    foldU :: (b -> b) -> b -> (forall s. U s -> (U s -> b) -> r) -> r
    foldU f b0 cc = cc (U (iterate f b0)) (head . unU)

    I am actually not totally sure whether this new mechanism buys us anything in general, or if there is always some encoding like this.

  2. Can’t you get the same thing with comonads that have somewhat stricter than necessary counit and/or cobind? A strict counit would keep pure (non-comonadic) code from having references to the past in its unevaluated thunks, which sounds like the problem you’re having.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s