Calling all software engineers who know basic cate...
# thinking-together
n
Calling all software engineers who know basic category theory: some applied category theorists in the US are organizing a hackathon to explore how the theory of polynomial functors can be applied to software development (new programming libraries and/or languages). The attendees would be a mix of software engineers (who know category theory) and category theorists. If you'd be interested in attending or brainstorming about such a hackathon let me know. I've offered to help organize it, but we need more input from software engineers. šŸ™‚ This would be an in-person event in the US, taking place ~March next year. There is a short course and book draft on the category of polynomial functors, outlining its applicability to interactive systems and databases. I expect these applications will be the focus of the hackathon.
šŸ¤” 1
d
I’m interested in this, but I am only familiar with the basics of CT. FYI: I’ve been learning what I can about generating code from laymen-defined models+properties where the generated code ā€œsmartlyā€ chooses between both runtime (based on collected metrics) and static (based on machine model) strategies (such as sort algorithm, data layouts, GPU vs. CPU targeting, batch/row sizes, etc). There’s also a very difficult problem on providing feedback or even choices when ā€œthingsā€ are over-constrained/non-feasible. Any thoughts on if Poly could be a helpful way to model this problem? In the Poly book, they restrict the lens structure in a way I don’t understand, so I don’t know if it can model more complex optics like monadic lenses (which is one way to model+execute RT strategy decisions). I also really don’t understand the implications of things like ā€œpreserving op-cartesian arrows.ā€
n
I’ve been learning what I can about generating code from laymen-defined models+properties
It sounds like you're interested in compilers for high-level languages? Your description reminds me of MLIR, which aims to be a good framework for compiling programs from (vastly different) high-level domains, such as neural networks and hardware circuits. It definitely does all those static optimizations you describe. As for whether Poly can help with this: my hunch is no, not right now. (Disclaimer though: I'm not a category theorist, I'm just a software engineer who's been in contact with the book authors.) Poly is being investigated as a modelling language, but not as a compiler. The main challenge right now is connecting Poly back to everyday programming constructs. We've got an understanding of how it connects to type systems, I/O, and databases, but other important stuff like recursion is missing. It's unclear how deep the Poly rabbit hole goes; it's still very early days. That's why there's a hackathon being planned: to support further exploration!
I don’t know if it can model more complex optics like monadic lenses
Nor do I. I don't even know what a monadic lens is šŸ™‚
I also really don’t understand the implications of things like ā€œpreserving op-cartesian arrows.ā€
The book is mainly targeted at category theorists right now, and so its style is to list out a bunch of theorems on every aspect of Poly. Some of them have clear implications, some of them don't. My personal strategy has been to focus on the theorems that seem interesting to me as a software engineer šŸ˜‡.
šŸ‘ 1
d
Hah, well my current hope is that the compiler input isn’t a high level language, but a model (think more like minecraft or sketch) I’m looking for the right model(s) to slowly increase power/complexity, basically adding a dimension at a time (and trying to keep people thinking about the ā€œwhatā€ rather than the ā€œhowā€ when manipulating the model)
n
What do you mean by "model" here? That word has a lot of meanings! For example, how do you wish me to perceive Minecraft as a model? I see it as a fully-fledged interactive application! But if I were to think of Minecraft as a tool for making models, I can recall how people use Minecraft blocks to build physical models of locations and buildings. But those aren't models of interactive systems. You can also use Minecraft's redstone system to build circuits, but that's equivalent to a low-level programming language, so I don't see it as something special. And of course you can write mods for Minecraft, but that's just conventional programming.
d
Minecraft is a game where you have a model of a world, you can move around to look at different pieces of it, and manipulate it by doing certain actions (whose number and complexity grow over time) If you replaced the ā€œmodel of the worldā€ with a ā€œdirectoryā€, ā€œmoving around to look at different pieces of itā€ with ā€œclicking and scrolling in an IDEā€ and ā€œdoing certain actionā€ with ā€œadding/editing codeā€, then you get an open-ended game we call programming šŸ™‚. I used Minecraft here as a reference for two reasons: 1. ā€œAdding/editing codeā€ is all or nothing-- I’d prefer a growing set of manipulation operations (like several minecraft mods add) to avoid boilerplate without the user needing to know in advance about every operation to understand the model 2. Minecraft operations/views are built around certain guarantees of the ā€œmodelā€ (usually how different cubes will interact). In programming, the directory is so unconstrained we barely think about it; the only constraint (assumed) is that the files in the directories respect their extensions, so becomes a facsimile for some distributed AST.
n
I'd say a Minecraft world is a "world" or an "open system" (in the sense that it has state and I/O), not a "model of a world". The latter phrase suggests it's trying to accurately emulate (model) something external.
Minecraft operations/views are built around certain guarantees of the ā€œmodelā€
Right, I'd describe that as "the state obeys a schema" and "the interactions obey a protocol". The aforementioned Poly aspires to be a language for schemas and protocols šŸ™‚ (but it's not well-developed yet)