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.
Davi Sales Barreira (May 28 2024 at 17:01):Hello everyone. I was wondering if there are any resources on the use of Topos Theory applied to Functional Programming. I've been reading a bit on Topos Theory, and the texts tend to emphasize how toposes are used to relate global and local structures. I imagined that perhaps it could serve as a "canonical" way of representing data structures where one has nested contexts. For example, suppose we have geographical map inside another geographical map, and we want to define an interface that allows us to hop from one context to another. Perhaps Topos (or some other concept in Category Theory) can provide a clear framework for how to properly deal with such situations. I haven't been able to find references that try to apply Topos Theory to Functional Programming in the vein of Bartosz "Category Theory for Programmers".
Ryan Wisnesky (May 28 2024 at 17:49):one direct way is that the syntactic passage from a simply typed lambda calculus to a higher order logic is reflected in the semantic passage from a cartesian closed category to a topos (which adds a type of Propositions/subobject classifier to a CCC). An example paper in this line of work is Bell's "Notes on toposes and local set theories".
Eric M Downes (May 28 2024 at 20:27):Your description of the problem made me wonder if you have tried using just stalks of presheaves alone? Not that topoi wouldn't be appropriate, crudely stalks : topoi :: elements : sets, but what you describe (a kind of recursive contextual organization of local-truth organized by space/topology) seems spot on. Presheaves are available in haskell at least, although I would also recommend checking out Bewl an experimental system built in scala by @Felix Dilke, which I have not used but seems kind of like topos-theoretic ADTs.
Eric M Downes (May 28 2024 at 20:32):The paper Ryan W. referenced is here.
Davi Sales Barreira (May 28 2024 at 20:45):@Eric M Downes , what do you recommend for learning sheaf/presheaf theory?
Davi Sales Barreira (May 28 2024 at 20:45):BTW, thanks for both answers!
Peva Blanchard (May 28 2024 at 20:47):Slightly related is the blog post by David Jaz Myers and Evan Patterson on the propositional logic of subgraphs.
It is not exactly applying topos theory to functional programming, but applying topos theory to manipulate (query) graphs. Which is a fairly common data structure in programming.
The underlying categorical data structure is that of C-set. It's basically (op)presheaves.
Eric M Downes (May 28 2024 at 20:57):As far as learning about sheaves... I really love this book MacLane and Moerdijk and the stacks project is canonical. But first watch DJM's very accessible talk I linked above and if you are still psyched, before embarking on a year+ math quest, perhaps try and work through John Baez' series on topoi which heavily features sheaves and should be accessible if you worked through Bartosz' lectures on category theory and are willing to look up some math/topology syntax. Your ally in learning this could be @David Egolf as he has started an entire active thread for reading through the series. Can' figure out how to generate the link to that topic, but you can find it in the same channel/stream/zulip-organizer-thing as this.
Peva Blanchard (May 28 2024 at 21:02):Here is @David Egolf 's thread
Eric M Downes (May 28 2024 at 21:06):(Alternately, if you need to build a cool database fast maybe you could just hire Ryan's company -- categorical databases is his area of expertise :)
Davi Sales Barreira (May 29 2024 at 11:21):Thanks for the suggestions. I'm just a humble phd student, trying to improve my thesis :sweat_smile: