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.
Nick Smith (Apr 16 2021 at 07:24):Hi everyone, I'm new to this community. Apologies if the following is too big of a spiel.
I'm on a (very serious) quest to develop a programming system that can make software development more accessible and more scalable. I have a computer science background, but a keen interest in mathematics, and I'm looking for intuitions about how modern mathematics can inform the design of radically-new programming models. Unfortunately though, I'm a category theory noob, so to save me spending 2 years studying category theory in an attempt to answer the question myself, I'm looking for encouragements or warnings about how category theory can or can't help me (and which parts of it).
It's important that I spend a moment to clarify my perspective on programming, since a lot of the "popular" connections between category theory and programming relate to type theory and functional programming, and these connections aren't of obvious use to me.
Firstly: I definitely understand the value of type theory and formal verification of program properties, however my primary focus is on exploring wholly new programming paradigms (new kinds of languages) that allow humans to better harness the power of computers to achieve their goals. I don't see a means by which type theory can inform me about new programming paradigms.
Secondly: I'm not interested in new approaches to "functional programming", per se. This is a consequence of some of the guiding principles that are driving my quest:
Now, to return to my question :smile:. Does anyone have a feel for how category theory can inform novel programming paradigms, specifically paradigms where data isn't forced into hierarchical structures ("trees"), yet data can still be operated upon "in bulk"? Can order be an emergent or "dynamic" property of computation rather than an imposed one?
Are there concepts in category theory which can help me answer this question? Concepts which can ultimately be applied in practice? I'm very willing to learn whatever I need to!
Javier Prieto (Apr 16 2021 at 10:26):Can you give an example of what you mean by a "constraint language"? I feel like computing via fixed points could fit the bill since it has this general feeling of being implicit (and somewhat mysterious), but I'm just pattern-matching here
Verity Scheel (Apr 16 2021 at 12:10):Hm I don’t think ASTs are unique to functional programming per se, certainly any C++ compiler will also need an AST to represent the text it is parsing, but maybe it seems less hierarchical/stratified because it’s more boring (everything’s a statement). So most textual languages have an AST. But if you want to step away from textual languages, CT has invested a lot of research in graphical languages like string diagrams, making them more rigorous (as tools for mathematical reasoning, not necessarily computation). The flip side is that, since they are more freely structured, they are harder to implement cleanly in computers. But it’s certainly possible, if you want to put in the work.
Type theory is an incredible tool for studying languages in general. I know that FP works a lot with one particular family of type theories, but there’s no reason it has to be limited to that. Type theories are great for studying properties and structure of computer programs and other types of languages, establishing what you know and why you know it. Safety and meaning really come from type theory, in my personal view. But I think there’s actually a wider variety of type theories than you realize, and I wouldn’t discard using it as a tool for what you’re studying: you can be as creative as you want. I was just reading about the lambda-bar-mu-mu-tilde calculus, and they used types to ensure properties like well-formedness and termination. This particular calculus models a kind of producer/consumer duality that isn’t found in lambda calculi, but it also has deep ties to proof theory, and probably CT as well. These subjects tend to go together!
Jules Hedges (Apr 16 2021 at 12:13):It's likely that coalgebra is something you'd be interested in looking into
Jules Hedges (Apr 16 2021 at 12:14):In general, coalgebra is used to give category-theoretic foundations to "dynamic" things like computational processes that don't run input-to-output, but instead are ongoing and reactive
John Baez (Apr 16 2021 at 13:39):Javier Prieto said:
Can you give an example of what you mean by a "constraint language"?
I don't know what a "constraint language" is, but Choco is a package for doing constraint programming:
Choco is a Free Open-Source Java library dedicated to Constraint Programming. The user models its problem in a declarative way by stating the set of constraints that need to be satisfied in every solution. Then, the problem is solved by alternating constraint filtering algorithms with a search mechanism.
John Baez (Apr 16 2021 at 13:41):What the heck, I'll quote Wikipedia. This may be just a digression from the original question:
Constraint programming (CP)is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state the constraints on the feasible solutions for a set of decision variables. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties of a solution to be found. In addition to constraints, users also need to specify a method to solve these constraints. This typically draws upon standard methods like chronological backtracking and constraint propagation, but may use customized code like a problem specific branching heuristic.
Constraint programming takes its root from and can be expressed in the form of constraint logic programming, which embeds constraints into a logic program. This variant of logic programming is due to Jaffar and Lassez, who extended in 1987 a specific class of constraints that were introduced in Prolog II. The first implementations of constraint logic programming were Prolog III, CLP(R), and CHIP.
Instead of logic programming, constraints can be mixed with functional programming, term rewriting, and imperative languages. Programming languages with built-in support for constraints include Oz (functional programming) and Kaleidoscope (imperative programming). Mostly, constraints are implemented in imperative languages via constraint solving toolkits, which are separate libraries for an existing imperative language.
Spencer Breiner (Apr 16 2021 at 15:58):@Nick Smith said:
my primary focus is on exploring wholly new programming paradigms (new kinds of languages) that allow humans to better harness the power of computers to achieve their goals. I don't see a means by which type theory can inform me about new programming paradigms.
I'd be hesitant to identify a search for new paradigms with a search for new languages. Particularly if your goal is accessibility, "language" seems too low-level a concept. I would be looking harder at user interface (a la Bret Victor).
I also happen to think that UI/UX design is (i) the lowest-hanging fruit and (ii) the biggest barrier to entry for ACT, so I might be biased.
Georgios Bakirtzis (Apr 16 2021 at 17:08):It's not UI but it is about visualization which is closely related https://ieeexplore.ieee.org/abstract/document/6311404?casa_token=SVgxrOUIo90AAAAA:QoEgxZGQ24POQ-MmiMLJGr9hepW47bSOpQ42cO5Lfa8OiugcvVWBMF8znqntv0BJZC6OV4OahP8
Georgios Bakirtzis (Apr 16 2021 at 17:08):You might be interested.
Georgios Bakirtzis (Apr 16 2021 at 17:11):I think modeling and synthesis of code from visual or textual models might also fit this question but I'll have to think about it more.
Nick Smith (Apr 17 2021 at 00:15):@Javier Prieto John's Wikipedia excerpt summarises "constraint programming" in broad terms. Regarding constraint languages, these aren't as popular (sadly, IMO), but MiniZinc is probably the canonical example.
@Nick Scheel Sorry, I didn't mean to imply that ASTs were related to functional programming in particular. Yes, all textual programming languages (that I know of) are based on ASTs, due to the limitations of textual syntax. Regarding string diagrams et al, you're right that they're probably closer to what I want, and I appreciate their lack of hierarchy! But there seem to be many kinds of string diagrams/categories. They're an interesting syntax, but don't give any hints about new semantic possibilities, right?
@Jules Hedges Awesome thanks, I'll pay attention to coalgebras. Regarding modelling dynamic processes, I've also noticed @David Spivak has been really excited about polynomial functors ("Poly") for that purpose, though I have no idea how they work. Any idea about those?
@Spencer Breiner You're right, there's more to accessibility than languages, and I admire Bret Victor's philosophy greatly. In my project, I'm focusing on all of semantics, syntax, tools (the UI), and environments (the OS). However, I think this community might have the most knowledge about the first two :smile:, and I believe they are the biggest challenge. Languages are the foundation upon which "higher layers" like tools and environments are built, and I think the state of languages is pretty dismal. All of the programming paradigms we use today have been in wide use for decades, and all we seem to know how to do is "remix" them. Meanwhile, it's still incredibly hard to develop high-quality software, for novices and experts alike. That's why I wholeheartedly believe we need new paradigms.
@Georgios Bakirtzis Thanks, that looks like an interesting paper! I'll have a read.
Nick Smith (Apr 17 2021 at 07:09):I've actually found a paper on "coalgebraic logic programming". Definitely on my reading list now!
Fabrizio Genovese (Apr 17 2021 at 09:06):A bit of self shilling: statebox.org tries exactly to implement a different programming paradigm using category theory. :smile:
Javier Prieto (Apr 17 2021 at 09:29):Nick Smith said:
Regarding constraint languages, these aren't as popular (sadly, IMO), but MiniZinc is probably the canonical example.
Doesn't Prolog count? That's the only one I know from the wikipedia page on constraint programming, so I guess it's kinda famous
Nick Smith (Apr 17 2021 at 10:44):@Fabrizio Genovese I've stumbled onto that before. Guess I should revisit it! But can it run Tetris? :stuck_out_tongue:
Fabrizio Genovese (Apr 17 2021 at 10:44):Yes, it can
Fabrizio Genovese (Apr 17 2021 at 10:44)::grinning:
Nick Smith (Apr 17 2021 at 10:45):Show me how :hushed:. Where do I find the Tetris tutorial?
Nick Smith (Apr 17 2021 at 10:51):@Javier Prieto Prolog (and other logic languages) barely count. They can express a very limited form of constraints, and Prolog is mired in imperative features that limit its declarativeness.
Nick Smith (Apr 17 2021 at 10:53):There are some research languages that do constraints "better", but I think MiniZinc is the purest example out there.
Fabrizio Genovese (Apr 17 2021 at 12:00):Nick Smith said:
Show me how :hushed:. Where do I find the Tetris tutorial?
It means that it has the capabilities of doing so, exactly as you can play tetris in Excel. It doesn't mean that someone worked it out yet
Fabrizio Genovese (Apr 17 2021 at 12:01):We'll start opening up the software to an invited audience soon :smile: