A thread on Poly!

Poly is one of the hottest topic in ACT right now: Several research groups are working on it, more or less ignognito.

Poly is the category of polinomial functors and natural transformations between them. 1/n

This category is cool for a lot of reasons: It has a lot of good properties, plenty of monoidal structures interacting with each other, it is equivalent to the category of containers, but most important of all its morphisms can be thought of as dependent lenses. 2/n

Everyone in ACT knows that this has been the year of optics. It turned out that a lot of stuff (open games, AI, machine learning, databases, ...) composes optically. Dependent lenses are particularly powerful optics, and indeed a lot of this stuff can be done in poly. 3/n

Poly has been around pretty much since forever, but it's David Spivak and David Myers that pointed out how Poly has lots of stuff relevant for ACT into it.

In particular, atm it is clear that you can do both dynamical systems and databases in Poly, at the same time. 4/n

Indeed, you can see morphisms in Poly as "mode dependent dynamical systems". These are dynamical systems that rewire themselves as time goes by. So the wiring is not fixed, it really depends on the info going around on the wires. 5/n

This is hyper powerful. I am pretty sure that, in terms of expressivity, Poly can perform Turing complete computation.

Ok, so we found a super general thing, maybe "universal" in expressing lens-like stuff. Set is universal as well, and we abhor it, so what's the point? 6/n

Indeed, when stuff is so powerful, I tend to be scared. I do prefer restricted settings where stuff is decidable, and Poly is very far from this.

Here is what I believe is the real advantage of Poly: It rocks when you implement it.7/n

Indeed, if you have a categorical framework that subsumes 50% of what is relevant in ACT right now, the first thing you wanna do with it (imho) is implementing a programming language based on it. The internal structure of Poly will work as the typechecher. 8/n

All things considered, the real bet here is that we could use poly to create the first ACT-centered programming language. Mind me: I said ACT-centered, not CT-centered. Here lie orders of magniture in complexity reduction, and will probably make ACT practically viable. 9/n