13 ms·
Seven Sketches in Compositionality: An Invitation to Applied Category Theory
- wisnesky 7y agoThere is up to $1.5M USD available for start-ups who want to solve business problems with category theory: https://conexus.ai/ventures https://conexus.ai/ventures and there is an open-source implementation of the data migration sketch from that book here: http://categoricaldata.net http://categoricaldata.net
- carapace 7y agoWhat a bizarre (in a good way!) and interesting opportunity. You're Dr. Ryan Wisnesky, eh? Are y'all familiar with Conal Elliott's "Compiling to categories" work? http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ > Abstract > It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages. I'm an independent (amateur) researcher working in the space of Categorical languages (Joy, my project: http://joypy.osdn.io/ http://joypy.osdn.io/ ) I sort of "backed into" the categorical aspect of Joy when implementing type inference ( http://joypy.osdn.io/notebooks/Types.html http://joypy.osdn.io/notebooks/Types.html ). You can evaluate a Joy expression in the "category of values" and get a computation, or in the "category of stack effects" and get a type signature. Elliott is converting Haskell code into Joy-like point-free form and implementing several interesting Categories. Without going into a lot of detail, I became interested in Prolog (for implementing a Joy compiler) and went down a bit of a rabbithole. ( https://hg.sr.ht/~sforman/Thun/browse/default/thun https://hg.sr.ht/~sforman/Thun/browse/default/thun ) Now I am in some sort of transition phase between what I used to be (mostly Python programmer) to what I'm becoming, a Prolog and Joy programmer. Anyhow, do you think it would be worthwhile for me to apply? I have a kind of patron right now, but it would be nice if he had some help.
- wisnesky 7y agoAbsolutely, and I would encourage you to contact us offline first to discuss related work in this space - there is indeed a lot, because the category of CQL schemas forms a BCCC and for each schema S, the category of S-databases forms a topos, briefly described here: https://www.categoricaldata.net/cql/haskell.pdf https://www.categoricaldata.net/cql/haskell.pdf. So CQL is expressive enough to interpret the STLC and higher-order logic in a few different ways.
- carapace 7y agoI've just been reading up on your CQL. Damn son. So I feel like I'm building a sand castle and you guys have built Howl's Moving Castle. Seriously, CQL is amazing. You've done everything I had hoped to data-wise and on such a firm and rigorous foundation. My hat's off to you. I'm still going to get in touch, because I'm really interested in what you're doing, but maybe I'm not in the right place to apply for anything yet. (We can talk about it.) The Joy system I'm playing with has some UI ideas inspired by the Oberon OS and Jef Raskin's "Humane Interface", but other than that I'm not sure there's anything there for you. Joy itself might be a good UI "macro" language.
- j88439h84 7y agoThis looks cool. Is there an append-only version of these database tools? (In the sense of never overwriting or deleting a value, only adding a new value with a new timestamp.)
- delish 7y agoWhen I first saw this comment it was downvoted. wisnesky is one of the main contributors in the applied category theory world, and one of the reviewers for Conexus's FRP. IMO it's reasonable to advertise for that on a post about Seven Sketches. I've been meaning to work with CQL to see if it can make XML-to-other-stuff data migration easier. I can picture in my mind how I want the migration to go, but/and it's always a lot of error-prone, one-off work in $work_lang.
- edwintorok 7y agoFWIW I originally found out about the Seven Sketches paper from this site: http://lambda-the-ultimate.org/ http://lambda-the-ultimate.org/ Your message about funding research/products would probably be of interest to LtU readers, but their site policy is usually against ads. Perhaps you could send a message to http://lambda-the-ultimate.org/user/1 http://lambda-the-ultimate.org/user/1 and ask whether it would be appropriate to post about your venture accelerator and where/how to post it?
- deleted 7y ago[deleted]
- adamnemecek 7y agoCategory theory is all about adjoints. What's an adjoint? Adjoint and a norm give you the inverse.
- Koshkin 7y agoCan you please elaborate.
- benrbray 7y agoNot sure what the poster had in mind, but I will refer you to some notes by a geophysicist about intuitively understanding adjoints:http://www.reproducibility.org/RSF/book/bei/conj/paper.pdf http://www.reproducibility.org/RSF/book/bei/conj/paper.pdf
- ginnungagap 7y agoThis talks about adjoints of operators, which is where the category theory terminology comes from, but a pretty different concept overall
- blumomo 7y agoThe book is downloadable as PDF and reads very well on Kindle. As chapters are recognized as such and it's easy to directly open any of them. I'm looking forward to study the contents in detail as I hope to improve my abilities to build software abstraction layers with the described theory.
- Koshkin 7y agoThe thing is, Category Theory and the practice of programming are too far apart. To create a reasonable application of some notion of CT in software development, the notion must be first thoroughly digested by the theoretical computer science, with the usual stress on the computational efficiency and the constructive formalism; the result of this must be a set of well-understood computational schemes - data structures and algorithms; only then one can hope to arrive to a design of a universally useful library, in a given programming language, that could withstand criticisms and the test of time. This is similar to the distance between, say, knowing Analytical Mechanics on the one hand and being able to build an efficient and economically viable internal combustion engine on the other...
- ardani 7y agoTell me about it, I've been trying to develop a complete visual metaphor to category theory for years. Edit: you're missing that to formulating the hard- and software stack we already have in a category theoretical metalanguage solves that problem also - but that requires overcoming DRM and lacking tooling for software analysis.
- schwurb 7y agoDunno if that is helpful to you, but one tip from the link related it to always think of new CT constructs in terms of partially ordered sets if possible. They make for nice visualizations and are generally quite intuitive.
- blumomo 7y agoThanks a lot for your thoughtful warning!
- joe_the_user 7y agoI really like the way this book jumps between concrete problems and general tools for their solution. I understand this book is about applying category theory tools and not about category-theoretical-language like Haskell but these are popular here so it brings up the topic. But this brings up a question about concrete structures and abstract qualities of programming languages. Looking at, say, chapter 2, you have the problem of finding the least-costly recipe for a given task mapped to the abstract monoid structure. Now, I understand a very nice approach where you essentially go: Concrete real-world-problem -> abstract-problem, then utilize standard-abstract-facility for solving abstract-problem. If the abstract-facility is incorporated into the language itself, this can happen "effortlessly" and nearly invisibly. But, this happy scenario can become an unhappy scenario when you have done all that, it works well, when suddenly you find the concrete problem has qualities that are completely irregular and don't fit the abstract model at all. Suppose cost of recipes varies in some weird, ad-hoc fashion, etc. What to do? Data behaving in a regular fashion is the font of mathematical structures and allows powerful tools. But change that regular behavior to something less regular and you may or may-not get something ammenable to further abstract manipulation. The thing is, if you take "recipes" becoming "monoids" and have your own library for deriving a category theoretical solution, and if then what "recipes" do suddenly is less category theoretical, then you can change your library - perhaps in a way that does violence to the concepts but still happens to work. But if you take "recipes" and use the built-in language facilities for the monoidal properties of a problem, you may have a lot more trouble modifying the map between concrete problem and abstract solution. And certainly, the modified library may be a long-term terrible solution if you expect the problem to grow. But suppose you don't, suppose you can benefit from exactly this level of abstraction and ad-hoc modification and would pay a bit for a lot of abstraction. Is there something I'm missing in this criticism?
- mathgenius 7y agoAll models are wrong. You are free to decide if this is a bug or a feature of any particular model.
- dmix 7y agoIf anyone makes a book of recipes that look like the diagram on page 4 of the lemon pie, especially an interactive one for the web/tablet, I’d buy it. Maybe a good side project/business. It makes so much more sense displayed visually than a fixed incremental list. It’s possible you could generate them automatically with some NLP and hand tweaking.
- dunham 7y agoThere was once an iOS app called "Baking with Dorie" that had a similar presentation. It caught my attention because I was interested in novel ways to represent recipes. It's no longer in the app store, but there are a few reviews out there with screenshots, e.g. http://omgyummy.files.wordpress.com/2011/09/image-4.jpg http://omgyummy.files.wordpress.com/2011/09/image-4.jpg It seems to me that if you added time to one of these wiring diagrams (for the recipe use case), you would have a Gantt chart. This might also be leveraged to plan parallel processes in a recipe (e.g. making the second part of a mole sauce while waiting for the chilis to soak). For complex recipes or meals, I could also see using the wiring diagram to represent a high level flow between sub-recipes, and then drilling down into a node to view the diagram for that sub-recipe. You might be able to mock this up with "milanote". In the past I've built a dependency diagram for a complex dinner (dishes from the Eleven Madison Park cookbook) by scanning my markdown transcription of the recipes and generating a 'dot' file for graphviz. For planning meals like this, I think a Gantt-like representation would be useful. Some components were made a day or two ahead, some same day, and some steps had to be executed at the last minute.
- small_lemma 7y agoYou may be interested in the book "How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics" by Eugenia Cheng. It's a book that relates concepts from cooking to Category theory.
- emmelaich 7y agoYou were downvoted for some reason (automatic?) Here’s a wiki page for that book https://en.wikipedia.org/wiki/How_to_Bake_Pi https://en.wikipedia.org/wiki/How_to_Bake_Pi
- eadan 7y agoPrevious HN discussion [0], and associated lectures [1]. [0] https://news.ycombinator.com/item?id=19701767 https://news.ycombinator.com/item?id=19701767 [1] https://ocw.mit.edu/courses/mathematics/18-s097-applied-category-theory-january-iap-2019/index.htm https://ocw.mit.edu/courses/mathematics/18-s097-applied-cate...
- webdva 7y agoThanks for sharing this, because it looks like it will be useful especially to those wanting to learn how to apply theoretical concepts.
- sunstone 7y agoSo, applied abstractions then?
- fernly 7y agoOK, moderately well-read in software engineering but not in math; experienced programmer; start reading the intro, sounds promising; but early on I find some presentation problems which I think are going to impede you reaching the audience you describe in the first few paragraphs. Just a bit of a commentary here; if I persist I may send a more detailed review -- although I note that there is no invitation to do so, or address for comments, in the Introduction? Top of p.iv, "almost no introductory material available on monoidal categories." Wait, it was all about categories, now it is suddenly monoidal ones -- what is monoidal, is that a subset of the book subject, or a more precise term? Badly need a definition when first introducing a new term. (Actually, that just highlights the point that the term "category" has been assumed and not defined to this point -- despite the audience not being expected to know what it is.) Lemon pie diagram: of _course_ I can grasp the basic idea, but in what sense does the diagram illustrate category theory? Where are is the category (categories?), is it the pie, the lines, the nodes? It's probably blindingly obvious _after you understand the topic_ but at the opening of the book, the point needs to be explained even if the explanation seems redundant to the author. Top paragraph on p.v flirts with a definition but doesn't actually define anything. Is a category "structures and coherence"? One "involves" (vague) "a collection of objects, a collection of morphisms relating objects, and a formula for combining any chain of morphisms into a morphism" and OK, here is a hint of familiar ground: this sounds a lot like category theory might be a generalization of classes, instances and methods, and functional composition, of software engineering. But the sentence about chains of chains ending in a happy "That's it!" doesn't really seem to follow. Onward. Bottom of page 1, we finally get to some substance, although I really don't like the "Y is a meter" explanation because that whole paragraph kind of bodges the distinction between italic-capital-letter X and Y, which I am kinda sure you intend to represent classes or domains, with the word "object" which my prior training really wants to confine to singular instances of a domain. So what comes out of the map isn't a "meter Y" but "the reading displayed by the meter Y" but that doesn't work either. Anyway, very shortly you drop in another new notation, "functions f from big-R to big-R" What does the big-R mean here? I'm casting about -- real-world-objects? set of Real numbers? Probably real numbers because the following features are about arithmetic comparisons and operations. But say it, dammit. Order-preserving, ok, but -- why "metric-preserving"? How is absolute-difference a "metric"? But... this is an exercise and a challenging one, and I'm intrigued. Later.