Seven Sketches in Compositionality: An Invitation to Applied Category Theory

by edwintorok • 7 years ago

294 36 7 years ago

wisnesky2• 7 years ago

There is up to $1.5M USD available for start-ups who want to solve business problems with category theory: https://conexus.ai/ventures and there is an open-source implementation of the data migration sketch from that book here: http://categoricaldata.net

carapace2• 7 years ago

What 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/

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/ )

I sort of "backed into" the categorical aspect of Joy when implementing type inference ( 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 ) 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.

wisnesky2• 7 years ago

Absolutely, 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. So CQL is expressive enough to interpret the STLC and higher-order logic in a few different ways.

delish• 7 years ago

When 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.

edwintorok2• 7 years ago

FWIW I originally found out about the Seven Sketches paper from this site: 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 and ask whether it would be appropriate to post about your venture accelerator and where/how to post it?

adamnemecek• 7 years ago

Category theory is all about adjoints. What's an adjoint? Adjoint and a norm give you the inverse.

Koshkin2• 7 years ago

Can you please elaborate.

benrbray• 7 years ago

Not 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

blumomo2• 7 years ago

The 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.

Koshkin2• 7 years ago

The 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• 7 years ago

Tell 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.

blumomo2• 7 years ago

Thanks a lot for your thoughtful warning!

mikhailfranco• 7 years ago

True, e.g. whatever happened to SRI/Kestrel Specware?

Guthur• 7 years ago

The thing is that the gulf between CT and other branches of math is also there. CT maybe be generally capable of specifying any given problem but the further you branch away from it the more convenient it is for individuals to use a more domain specific language.

The simple fact is that CT is not a linga franca no matter how much advocates would like it to be.

joe_the_user• 7 years ago

I 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• 7 years ago

All models are wrong. You are free to decide if this is a bug or a feature of any particular model.

dmix• 7 years ago

If 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• 7 years ago

There 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

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• 7 years ago

You 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.

enobrev• 7 years ago

Not exactly the same but Cooking For Engineers[1] has a format that reminds me of this. I've no personal affiliation besides liking the Mac and Cheese recipe.

1: http://www.cookingforengineers.com/

eadan• 7 years ago

Previous HN discussion [0], and associated lectures [1].

[0] https://news.ycombinator.com/item?id=19701767 [1] https://ocw.mit.edu/courses/mathematics/18-s097-applied-cate...

webdva• 7 years ago

Thanks for sharing this, because it looks like it will be useful especially to those wanting to learn how to apply theoretical concepts.

sunstone• 7 years ago

So, applied abstractions then?

fernly• 7 years ago

OK, 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.

kidintech3• 7 years ago

I agree that to an inexperienced reader, most of your points would be valid. The downside is, it would be too verbose (imagine defining what big R is, for example). It being too verbose would stray away a different subset of readers, which arguably is more invested in learning (the number of readers that know what R and a monoid are but not category theory).

I think that the best way forward in your case is simply googling terms that the writers took for granted and which you don't understand (a monoid, for example), because the book material is one of the best I've seen on category theory.

CuriousSkeptic2• 7 years ago

While a monoid in abstract algebra is easy enough to understand from Wikipedia. Googling for monoids in the context of category theory could easily land you at nlab I.e https://ncatlab.org/nlab/show/monoid+in+a+monoidal+category I’m not sure that’s helpful to new a learner of the subject.

I recall that my personal experience of learning about CT was unnecessarily difficult due to being thrown into a bunch of definitions way to soon. (Which is understandable since there isn’t much else to it.) but I needed to un-learn my preconceptions about what information the theory encodes first, which was rally hard. Understanding that objects and morphisms are really _only_ about composability and _nothing else_ is challenging when your mind desperatly wants to see concrete thing like sets or numbers or what have you in those objects. Definition don’t help much until you can shed that urge. (To new learners I suggest to think of “objects” as the number of dots on domino tiles, or the poles of magnets, they describe where things may, or may not, compose, nothing more. category theory is just about naming patterns and rules of composition)

In particular even knowing the existence of monoidal categories is a distraction when getting to grips with how catgories as such generalize and abstracts monoids.

brohee• 7 years ago

A glossary as an annex sounds like a way to address this... Big-R and monoid would definitely warrant an entry.

edwintorok2• 7 years ago

There is a link for posting comments/feedback on the main arxiv page: https://docs.google.com/document/d/160G9OFcP5DWT8Stn7TxdVx83... There are ~381 comments there already, please post yours: it looks like the authors are genuinely interested in listening to feedback and addressing them perhaps in future revisions of the book.

Seven Sketches in Compositionality: An Invitation to Applied Category Theory

Related Stories