how good is Poly for dynamical systems, really? · theory: applied category theory

As much as I love the category, I'm noticing how bizarrely frustrating it is to write a mode-dependent dynamical systems (a reservoir computer in my case) using Poly constructs. When it comes to generating actual numbers for something nontrivial, debugging becomes a nightmare. It takes several minutes to do the plumbing necessary just to get the outer system to output information I can actually analyze.

Something obvious only happened to occurr to me this week: there's nothing Poly can do that Set can't, really. A dynamical system is just a morphism? Great, it actually is just a morphism in Set also (albeit one that is a giant composition of functions). If you care about type safety, just write Haskell code and use Debug.trace when developing something.

I'm asking this with love of course. I've been excited about the category and have loved working with it, but debugging it versus debugging a little matlab benchmark has caused some existential angst. "Why is anyone even doing this? is it just a cute coincidence that if you take a subcategory of the yoneda embedding you preserve the ability to express dynamical systems? is this actually practical?" etc.

Jules Hedges (Apr 28 2023 at 15:26):

... I probably have some things to say about it, but probably not until tomorrow

André Muricy Santos (Apr 28 2023 at 15:27):

i should note that I have been a programmer for 11 years and have only gotten into category theory about a year ago (and in a very leisurely way. watching bartosz lectures and "reading" topos blog posts without understanding anything). i'm sure i don't have the instincts that someone like Spivak has but i feel like by now I should have "seen the light" and somehow grasped how obviously better Poly is for expressing certain things (i.e. it actually is more natural/practical).

Jules Hedges (Apr 29 2023 at 15:41):

It would be very helpful to know a bit more about what you're doing, ie. what kind of things you're modelling and why, and what language, libraries etc you're using

Jules Hedges (Apr 29 2023 at 15:42):

I'd guess that quite a lot of your trouble is coming from the general phenomenon of compositional modelling being very hard at first. It's kinda like learning OOP all over again, except you have to invent all your own design patterns because nothing is standardised yet

Jules Hedges (Apr 29 2023 at 15:44):

For comparison: I'm not using Poly, but I'm using categories of optics which are closely related and share many of the same features. We use Haskell with a hand-rolled implementation of optics, with the core stuff using optics but not hesitating to fall back to plain Haskell whenever it's more convenient for something

Jules Hedges (Apr 29 2023 at 15:48):

The fact that all the data in Poly is "really" just data in Set is a general fact, if you push this to the extreme it becomes the straw-man argument "why are you using language X, assembly/Fortran/C/etc is Turing complete so you can just work there". At the other extreme there are also usually good reasons not to work in the most advanced language available (this fact applies to mathematics as well as software engineering!) - so everybody has to make a non-trivial engineering choice for these kind of tradeoffs

André Muricy Santos (Apr 29 2023 at 17:57):

I'll need some time to collect my thoughts in order to properly reply as well. in particular i want to actually finish this damn thing. will probably say more tomorrow :+1:

André Muricy Santos (Apr 29 2023 at 18:01):

I do want to say that yes, i understand this, i didn't make my point very well very well. I guess i was attempting to contrast the difficulty i'm facing in actually writing code using Poly with how naturally it "claims" to be able to represent the things im trying to represent. I tend to roughly interpret "this framework is good for expressing X" as "this framework has a very nice type system", which is why i mentioned type safety in haskell.

Matteo Capucci (he/him) (May 02 2023 at 21:33):

I'll point out this wouldn't be the case if one were working in a programming language which 'compiles' to Poly. Instead, atm one has to manually be the compiler and that impacts the practical appeal of Poly constructions. But this is not specific to Poly, but to every category whose internal language is simple and expressive but different from standard type theory.

Matteo Capucci (he/him) (May 02 2023 at 21:33):

The real deal is programming in the categories one'd like to use, but that's mostly sci-fi currently

Fabrizio Genovese (May 02 2023 at 22:06):

What you are really saying here is that the bare minimum to make category theory useful in software applications is:

In general, any programmer will concur on the fact that the 'language' (or more appropriately 'the core machinery' in this case) is just the tip of the iceberg. There's a lot of stuff around it to make the language practically useful, the bare minimum probably being a linter, a packet manager, syntax highlighting, virtual envs etc.

So 'we can do dynamical systems with Poly' won't be really 'we can do dynamical systems with Poly' until all these further pieces of the ecosystem are implemented. And that takes time.

Fabrizio Genovese (May 02 2023 at 22:10):

If you want a real-world example of how this looks in practice, take a look at Rust. Rust has probably the most well-developed infrastructure around at the moment, and represents a good standard of 'how these things should look like in the best possible scenario'. If you come from Haskell, which is already a language with a quite developed ecosystem, programming in Rust will basically feel like magic.

Jules Hedges (May 03 2023 at 08:48):

I don't think this is necessarily always the case, depending on the host language and the structure you're implementing libraries can do just fine, for example AlgebraicJulia seems to do well

Jules Hedges (May 03 2023 at 08:49):

Poly suffers from requiring either dependent types in the host, or rolling your own typechecker for a fragment of dependent type theory, or faking it (which comes with its own downsides)

Fabrizio Genovese (May 03 2023 at 10:49):

Well, if you have a DSL embedded in a language with a nice ecosystem, you can clearly leverage on that, but it is not always going to cut it. For instance, syntax highlighting will be missing for your DSL, as will be advanced debugging features.

Fabrizio Genovese (May 03 2023 at 10:51):

And yes, libraries can be fine but they sill have to be packaged in a way so that they can leverage the host language packet manager. Ideally, if Poly allows to represent dynamical systems, I'd like to have libraries of 'already battle-tested' dynamical systems that I can install by just using the host language packet manager from the command line. The alternative would be manually downloading them from this or that repo, which obviously also works, but the point of my comment was exactly that 'also works' may not necessarily mean 'having a nice development experience'.

Henry Story (May 03 2023 at 13:35):

I followed a few of the poly courses, and I was wondering if that maps well to actor systems? It seems to from afar, because poly allows nodes to have state, contain other nodes and change behavior. And nodes can be named I think and so composed.
Actor systems such as Erlang or akka are similar to object oriented programming but can work in parallel. Instead of method calls one sends messages from one actor to another. In Akka each actor can change their behavior and spawn children, which can be thought of as contained in the parent actor. In akka actors are named with URLs allowing one to connect actors that were not previously connected.
I have a thread on actors here https://twitter.com/bblfish/status/1358103100104572930

Really great overview of the history of computing and the emergence of the Actor model by Carl Hewitt. "Actor Model of Computation: Scalable Robust Information Systems" https://arxiv.org/abs/1008.1459 ( @ThePatHayes and @v_sassone's works are cited) "The Actor Model integrated:" https://twitter.com/bblfish/status/1358103100104572930/photo/1

- The 🐠 BblFish (@bblfish)

Ryan Wisnesky (May 04 2023 at 15:10):

Is Poly really that different than standard type theory? Via things like "Martin lof categories" https://core.ac.uk/download/pdf/82087952.pdf using Poly to me seems a lot like just writing down inductive/coinductive types in e.g. Coq/NuPRL/etc. In fact Josh Meyers is trying to prove things about Poly in Coq as we speak. I'm guessing NuPRL will be a lot easier tho

Matteo Capucci (he/him) (May 04 2023 at 18:57):

You can definitely interpret MLTT in Poly, but most of the interesting stuff in Poly makes use of the other, 'non-classical' structures (like

\otimes

and

\circ

). Those would require new syntax to be used with the same ease you use

\Sigma

and

\Pi

.
Also there's the whole thing of the bidirectionality, which is an interesting programming design challenge (as @Jules Hedges knows more than well)

Ryan Wisnesky (May 04 2023 at 19:04):

There is a nice "notation" mechanism in Coq to extend syntax, for example, you can use it to add monad comprehensions to Coq, which are SQL-like syntax. So now I'm thinking adding Coq notations for those non-classical operations may be part of the contribution of the Coq development, thanks!

Matteo Capucci (he/him) (May 04 2023 at 19:12):

Matteo Capucci (he/him) (May 04 2023 at 19:13):

Ryan Wisnesky (May 04 2023 at 22:52):

Jules Hedges (May 05 2023 at 10:31):

Not true: I have it on good authority (ie. Fred) that Poly is not LCCC, so it's doesn't model

\Pi

types

Jules Hedges (May 05 2023 at 10:33):

Extracting a programming language and type theory from Poly (and dependent optics, the non-cartesian version) is a major thing I plan to work on in the near future, very happy to hear ideas about that

Jules Hedges (May 05 2023 at 10:33):

André told me yesterday that the underlying type theory used in the Scala compiler has dependent

\Sigma

(ie. records) but not

\Pi

, so that's one place I plan to look for inspiration

Henry Story (May 05 2023 at 13:06):

Any thoughts on my intuitions regarding Poly and Actors @Jules Hedges?
Perhaps as you work with Haskell you may not have been exposed to Actor languages like Erlang, but as a programmer you would have heard about thes as they such languages have been widely by Ericson to start with and now widely with companies like PayPal for example.

Jules Hedges (May 05 2023 at 13:52):

I'll need to think about that (maybe someone else has some thoughts in the meantime)

Jules Hedges (May 05 2023 at 13:53):

I wonder if the question can be usefully generalised to "to what extent can Poly be a model of concurrency?"

Jules Hedges (May 05 2023 at 13:54):

It certainly has at least one monoidal product that I think of as "parallel" in some sense (the one that David calls Dirichlet product, around here we sometimes call it the Hancock tensor product, I normally just call it the tensor product)

Jules Hedges (May 05 2023 at 15:04):

I'm not aware that any of the monoidal products on Poly admits a trace, which would be a standard place to start on a question like that

dan pittman (May 05 2023 at 17:55):

As someone who went from Haskell to Rust for his daily driver language, I can say that this is absolutely true. And it makes going back even harder (something that I am currently, actively struggling to do). I'm saying this to underscore your point, that the problem often lies between the elegance of the theory and the messiness of Real World Programming, and I wonder if this distance is what makes something like this hard to "get" in practice.

Henry Story (May 09 2023 at 16:56):

I am pretty sure that @David Spivak has mentioned Poly in the same breath as Dynamical Systems. So the structures you need should be there. I found this 3 year old talk on a quick search "Mode-dependent dynamical systems and polynomial functors" https://www.youtube.com/watch?v=U-W7GT0BUTU

Jules Hedges (May 09 2023 at 17:11):

Dynamical systems yes, I think that was even David's starting point for this line of work. It's the concurrent part that's not clear to me

Jules Hedges (May 09 2023 at 17:13):

Actually I'm not familiar with the actor model so it's very possible I'm jumping to conclusions and it's easier than I've suggested

David Spivak (May 09 2023 at 17:20):

David Spivak (May 09 2023 at 17:23):

I agree with people saying that it's difficult to program using Poly at the moment. That's like how it's difficult to actually program with the lambda calculus. Someone has to do the hard work of creating a Haskell-analogue. But I think there's huge potential there, especially for dynamical systems, but also for data migration and dependent type theory, all in one place.

Jules Hedges (May 09 2023 at 17:33):

That's good news. Is the idea that you get a model of

\Pi

types by picking a class of display maps? (Kicking myself a bit for not thinking of that earlier.) Do you know what the "correct" class of display maps is in Poly?

Henry Story (May 12 2023 at 12:17):

I posted on Twitter links to two or three papers on Actors from a Category Theory point of view, following conversations I had on Zulip.
This might make it easy for you to understand
https://twitter.com/bblfish/status/1567062264926150656

"strategies are presented as sheaves on a category of multi-party play, with forking (= a player dividing into 2) modeling parallel composition in the π-calculus. The coverage says that a play is covered by its sub-views = individual histories of players." https://lmcs.episciences.org/4069 https://twitter.com/bblfish/status/1567062264926150656/photo/1

- The 🐠 BblFish (@bblfish)

dan pittman (May 12 2023 at 18:34):

Ah, this is interesting. Trying to find a categorical expression for

\pi

-calc seems like the right path. There is also the join calculus which wikipedia says is a member of the family of

\pi

calculi, but my intuition for it was something closer to CRDTs [convergent (née conflict-free) replicated datatypes] from the dist sys literature, which are lattice-based so categorical semantics would, I imagine, be fairly straight forward—essentially posets.

André Muricy Santos (May 16 2023 at 15:03):

@Jules Hedges Now I can post what I was working on, because it FINALLY WORKS.
I was trying to model a reservoir computer, which is a recurrent neural network that learns how to predict nonlinear time series. It has two basic components: a reservoir of dynamics and a readout layer. The reservoir of dynamics is any large "box" containing a dynamical system with nonlinear dynamics (one doesn't have to understand it), so it's usually implemented via a recurrent neural network where all nodes are connected to all others (there's alternatives but I wont discuss the reservoir literature). The readout layer is like in a regular neural network: it reads from the nodes in the reservoir and multiplies some weights. The big advantage is that you don't train anything but the output layer, so no backprop shenanigans, you can just use linear regression.

The basic idea is, the output layer learns to represent the time series in terms of the dynamics of the reservoir, which is huge compared to the input so it ought to be enough to represent the time series. AFAIK reservoirs are also used for general computation, its part of a broader field of neuromorphic computation.

There's 3 stages: when youre feeding the data, then you hit the reservoir with part of your timeseries to predict to get rid of transient dynamics, then you make the readout layer loop back on the reservoir, and this last stage is when you count its output as a prediction. So in terms of poly, this to me suggested a mode-dependent dynamical system like in the first image linked.
PXL_20230516_144114703.jpg
and this is what I was trying to make work, but its problematic for several reasons. one is that the reservoir of dynamics should not have mode-dependence at all, because it just takes an input, multiplies with its weights, and produces an output, it never cares where stuff comes from. Second, the readout layer shouldn't care about "touching" and "going" states, it only accumulates enough data to train.

To cut to the chase, I tried to solve this by splitting up the "res" box in the image in two: the reservoir and the readout (second image
PXL_20230516_144129056.jpg) . but now I needed some outside "controller" to distinguish between the "touching" and "going" states, and what I discovered is that this is a mess in this setup: delays between the propagation of states started creating inconsistencies, and impossible combinations of states needed to be handled (the controller outputting "Touch" while the readout was still "training" - I didn't find a way to make such a thing unrepresentable, because all the wiring pattern lens has access to is the output of the systems). I tried some hacks with making the controller output "transition" states for a single timestep, but it became even more of a spaghetti mess. So I just went back to keeping the entire state (and associated counters) within the "res" box and having the "global" state centralized.

André Muricy Santos (May 16 2023 at 15:07):

on the other hand, poly (really just lenses, no mode dependence needed) makes it really nice to do something like altering parameters of a system "slowly" (i.e. at a timescale much larger than the system's dynamics), by just encoding the changing parameter as an input and having another box provide it. i did it for a little hodgkin huxley simulation and it's :ok:
as far as i can tell this is done in informal/hacky ways in normal dynamical systems modeling.

Stream: theory: applied category theory

Topic: how good is Poly for dynamical systems, really?

André Muricy Santos (Apr 28 2023 at 15:23):

Jules Hedges (Apr 28 2023 at 15:26):

André Muricy Santos (Apr 28 2023 at 15:27):

Jules Hedges (Apr 29 2023 at 15:41):

Jules Hedges (Apr 29 2023 at 15:42):

Jules Hedges (Apr 29 2023 at 15:44):

Jules Hedges (Apr 29 2023 at 15:48):

André Muricy Santos (Apr 29 2023 at 17:57):

André Muricy Santos (Apr 29 2023 at 18:01):

Matteo Capucci (he/him) (May 02 2023 at 21:33):

Matteo Capucci (he/him) (May 02 2023 at 21:33):

Fabrizio Genovese (May 02 2023 at 22:06):

Fabrizio Genovese (May 02 2023 at 22:10):

Jules Hedges (May 03 2023 at 08:48):

Jules Hedges (May 03 2023 at 08:49):

Fabrizio Genovese (May 03 2023 at 10:49):

Fabrizio Genovese (May 03 2023 at 10:51):

Henry Story (May 03 2023 at 13:35):

Ryan Wisnesky (May 04 2023 at 15:10):

Matteo Capucci (he/him) (May 04 2023 at 18:57):

Ryan Wisnesky (May 04 2023 at 19:04):

Matteo Capucci (he/him) (May 04 2023 at 19:12):

Matteo Capucci (he/him) (May 04 2023 at 19:13):

Ryan Wisnesky (May 04 2023 at 22:52):

Jules Hedges (May 05 2023 at 10:31):

Jules Hedges (May 05 2023 at 10:33):

Jules Hedges (May 05 2023 at 10:33):

Henry Story (May 05 2023 at 13:06):

Jules Hedges (May 05 2023 at 13:52):

Jules Hedges (May 05 2023 at 13:53):

Jules Hedges (May 05 2023 at 13:54):

Jules Hedges (May 05 2023 at 15:04):

dan pittman (May 05 2023 at 17:55):

Henry Story (May 09 2023 at 16:56):

Jules Hedges (May 09 2023 at 17:11):

Jules Hedges (May 09 2023 at 17:13):

David Spivak (May 09 2023 at 17:20):

David Spivak (May 09 2023 at 17:23):

Jules Hedges (May 09 2023 at 17:33):

Henry Story (May 12 2023 at 12:17):

dan pittman (May 12 2023 at 18:34):

André Muricy Santos (May 16 2023 at 15:03):

André Muricy Santos (May 16 2023 at 15:07):