Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: incremental computation

Verity Scheel (Mar 25 2020 at 07:00):

Hi, I was wondering if anyone has pointers to resources on incremental computation, especially in a CT/TT context? Is it an active area of research? It's something I'm really interested in, but I don't have enough theory or experience to make it happen, but I think it could be really cool in UIs and compilers and especially in interactive compilers (like structural editors for programming languages – that's something I really want to see happen, and I think some kind of incremental computation would do wonders to make it not only practical but advantageous over traditional text editing, which inherently has a fire-and-forget sort of nature).

Burak Emir (Mar 25 2020 at 07:13):

Can you clarify: do you mean you have some input that is translated, and upon local change, only those parts that are affected by the change are translated again? "those parts affected by the change" seems to be a poset of dependencies. I am not aware of a systematic treatment. The closest that comes to mind is https://pijul.org/model/ which is like git built on a categorical understanding of patches, with merges being pushouts.

Verity Scheel (Mar 25 2020 at 07:36):

Sure. This is the closest to what I was thinking: https://arxiv.org/pdf/1811.06069.pdf

What I’m looking for is how to calculate a change in the outputs based on a change in the inputs, in particular doing as little computation as possible. I don’t think just calculating the dependencies is too complicated, from a programming perspective.

Verity Scheel (Mar 25 2020 at 07:40):

As an extreme example, if I add one character to a string in a PureScript program, I should see a change that is the same character added in the corresponding string in the JavaScript output (since PureScript compiles to JS in a fairly direct manner), and ideally it would involve almost no recomputation in the compiler, since none of the types have changed, so none of the interesting bits of the compiler actually need to be reverified. But of course this is not how text-to-text compilers work, it would be a ton of work to overhaul an existing compiler to support, etc. etc.

Verity Scheel (Mar 25 2020 at 07:44):

I’ve seen Pijul before but haven’t deeply investigated it. I’d love to see how it would look if it were liberated from the textual paradigm, too ;)

Burak Emir (Mar 25 2020 at 07:56):

Thanks for sharing the paper, I am quite interested in datalog. Incremental computation in datalog is very specific, and it indeed looks like real work to apply approaches from that setting to compilers in general (yet I know people use datalog in compilers, for dataflow analysis), because compilers are complex. I haven't investigated Pijul further either, but mentioned it since one would have to represent a changed fragment of the program (the "unit of change", if you will), and if it begins with text, then the textual representation of changes could be helpful - is it one line? multiple lines? one file? multiple? Another thing I would freely associate is the unison language, where code is immutable, repository and execution environment is the same, and changes are a form of global update.

Verity Scheel (Mar 25 2020 at 08:17):

Unison is a good example of the direction I want coding to go. It seems like their form of global immutable code could achieve a sort of incrementalization through caching, where returning to old results is quick, whereas incrementalized computations would be optimized a little more for producing new results based upon the user’s specific interactions and wouldn’t necessarily keep so much data around. It’s a little like the difference between memoizing by building a hash table and memoizing by comparing to the last computed argument ...

Jules Hedges (Mar 25 2020 at 09:29):

I think this is the point where I yell "lenses" and then run away before anyone asks for details

Jules Hedges (Mar 25 2020 at 09:30):

"Delta lenses" are a compositional theory of incremental and reversible computation (if I understand) with some very nice category theory behind them, but probably very far from being application-ready: https://www.mta.ca/~rrosebru/articles/lfut.pdf

Maxime Lucas (Mar 25 2020 at 09:42):

I know that Yann Regis Gianas is thinking about this stuff. Here are some slides from one of his talks, with pointers towards other people's work: http://chocola.ens-lyon.fr/events/seminaire-2019-11-14/talks/gianas/

Philip Zucker (Mar 25 2020 at 13:23):

Incremental computation is an example in Compiling to Categories http://conal.net/papers/compiling-to-categories/. I'm not sure that it's explored in much theoretical depth there though if that is what you want

Verity Scheel (Mar 25 2020 at 17:29):

Thanks for the resources! At first glance the Régis-Gianas talk looks like it's closest to what I'm looking for, and it's really helpful that various approaches are discussed there. I'll have to investigate the other sources more.

Gershom (Mar 25 2020 at 17:34):

The linked "fixing incremental computation" paper describes some relation to the differential lambda calculus. There is a categorical formulation of the differential lambda calculus in the differential categories of Blute et al. On the purely-cs (not-categories) side of things, the richest body of work on incremental computation I know of is the stuff by Acar. Also related are "propigators" but they are sufficiently general that I think there's not too much good semantical work done on them.

There is some suggestive work by Foner and Paykin about a richer notion of the "derivative" of a data-type in an evented context which also may be able to be developed in a more rigorous way: https://www.youtube.com/watch?v=79zzgL75K8Q

Faez Shakil (Mar 26 2020 at 04:55):

Philip Zucker said:

Incremental computation is an example in Compiling to Categories http://conal.net/papers/compiling-to-categories/. I'm not sure that it's explored in much theoretical depth there though if that is what you want

There’s a working implementation too though I haven’t gotten the chance to work with this part of concat so far.

https://github.com/conal/concat/blob/master/examples/src/ConCat/Incremental.hs

Faez Shakil (Mar 26 2020 at 05:31):

Although with this general a type it’s tempting to imagine that anything you build can be incrementalized with the right instances

(.+^) :: a -> Delta a -> a

Verity Scheel (Mar 26 2020 at 05:41):

That's cool! Of course the question is how useful will it be? The automatic differentiation could actually be worse … although maybe in a lazy language the penalty is less. Unfortunately in Haskell most of the invariants you want to make use of for change structures are not explicit in the code, so the automatic system cannot take much advantage of it. But if you're differentiating a substantial subset of the program by hand, having the automatic stuff to fill in the gaps would definitely be helpful.

Verity Scheel (Mar 26 2020 at 05:44):

My question is how well are things like sum types supported? What's the best we can do for them? Of course product types are easy, but functions taking sum types are more interesting and much harder to differentiate. It seems like a change switching from one constructor to another is often discontinuous, in the sense that the new output is not much related to the prior output.

Faez Shakil (Mar 26 2020 at 06:00):

There’s this
(:+ is a type synonym for Either)

instance (HasDelta a, HasDelta b) => HasDelta (a :+ b)

So I’d assume sum types are as much under its purview as products.

Could you clarify what sorts of change invariants you’re referring to?

If you take a look at this function at the bottom, it’s pretty general.

inc :: forall a b . (a -> b) -> (a -> Delta a -> Delta b)

Given a function from a to b you get a function that gives you the change in b if you give it an a and a change in a.

Seems like the kind of primitive that would be very helpful to have if you’re building any sort of an interactive system where you only want to render whatever’s changed, for example

Verity Scheel (Mar 26 2020 at 06:10):

Oh, interesting, the change action for :+ isn't complete (in the sense of "Fixing incremental computation" – there is no way to get from Left to Right via the change action), so it sidesteps the issue I was talking about.

If you want a complete change action, it actually has to look something like type Delta (a :+ b) = (a :+ Delta a) :+ (b :+ Delta b), because in order to get from Left to Right (or vice-versa) you have to actually provide the new b value, and the automatic differentiation approach to it would have to recompute f (Right b) from scratch, which is the worst-case scenario.

Verity Scheel (Mar 26 2020 at 06:15):

So inc doesn't actually allow you to calculate a change from a Left value to a Right value, and you instead would have to recompute it

Verity Scheel (Mar 26 2020 at 06:25):

Another question I have in this area is reversing changes, which would be incredibly useful for storing undo/redo history, because you can cut down drastically on the data needed to store history, but you have to be careful that it's well-defined, so that you don't lose information while doing it. Does anyone know of research on this too?

I came up with a model for reversing changes that's based on patchAndReverse :: v -> dv -> Tuple dv v. The reason I do both at once is because, in general, it seems you have to know what v you're applying the dv to before you can know what the proper dv to undo it is. Sometimes you get lucky and can have a group structure on dv that means you can compute its inverse independently, but most of the time you need to know the structure of what you're changing before you can express how to get back there. Think of removing an element (from a list, map, etc.) – it doesn't really make sense to store the value of the element you're removing in the change action to remove it, but you definitely need to know its value to reconstruct it when reversing the change.
See my attempts here: https://gist.github.com/MonoidMusician/09ffe27e925525629a895af3c5b65f20 (wow, that's almost exactly 2 years ago now)

Verity Scheel (Mar 26 2020 at 19:29):

it doesn't really make sense to store the value of the element you're removing in the change action to remove it, but you definitely need to know its value to reconstruct it when reversing the change.

Actually, now that I think about it more, I think it actually might make sense to store the value you are deleting, for the reason mentioned above (you can now invert the change without knowing what it's applying to), and also because the element sort of serves as "proof" of the existence of the thing that you are deleting, which might prevent bugs, even just UI bugs like active-looking buttons that actually do nothing because they're trying to remove an element that doesn't exist.

Gershom (Mar 26 2020 at 20:55):

reversible stuff is quite different from incremental stuff, but here's one approach to it: https://arxiv.org/abs/1811.03678

Verity Scheel (Mar 26 2020 at 21:53):

oops, I meant reversing incremental changes, but reversible computation is very interesting too :smiley:

Reed Mullanix (Mar 27 2020 at 05:35):

Looking at the code posted, perhaps some sort of group (or monoid) action could work nicely? You could even potentially obtain some sort of rewrite system if the monoid or group is finitely presented!

Verity Scheel (Mar 27 2020 at 14:44):

Hi Reed! Yeah! I think the group action is a good idea, although it’s not clear if every change action lends itself to being so straightforward like I mentioned above. Some of the presentations do use monoid actions, others say it in all but name :wink:

Could you expand on the second part?

Reed Mullanix (Mar 27 2020 at 16:49):

So say you have some sort of source of state (to make this simple, let's say it's just a counter), and you have 2 actions that you can perform on it: replacing, and incrementing. Let's denote these actions $r_{k}$ and $i$, where $r_{k}$ replaces the value of the counter with $k$. Now, we can think about the free monoid generated by $r_{k}$ and $i$. However, just looking at the actions we have available, we have some laws that we can play with! For example, $r_{k} \cdot i = r_{k + 1}$, and $\forall a. a \cdot r_{k} = r_{k}$. So if we recieved a long string of actions that we needed to perform on the state, we could first optimize it by applying our laws to reduce it down to a simpler string.

Reed Mullanix (Mar 27 2020 at 16:55):

I guess this example isn't finitely presented, but rather recursively presented, but the idea still holds. You can optimize by simply writing out the laws, applying something like Knuth-Bendix, and getting out a rewrite system. To go even further, if you don't have a lot of reads, you could materialize the state on demand at later points in time, instead keeping a running log of all of the actions, that you optimize as you recieve

Mario Alvarez Picallo (Mar 28 2020 at 01:18):

Hi @Nicholas Scheel, I'm one of the authors of the paper you linked! You may also want to check out our follow-ups https://arxiv.org/pdf/1902.05465.pdf and https://arxiv.org/abs/2002.01091 - I'm not that involved with the "incremental" side of the project, instead focusing on the category theory and "geometry" of it but let me know if I can help at all.