Categorical sesh
Yesterday, I talked with @mkstra and @bgavran3. We have a shared interest in category theory, and there is a lot of overlap in the things that we are doing or have done in the past, so this talk served also as a brainstorming session.
Markus is interested in semantic analysis and extraction of knowledge from academic papers, and translating them into reusable, composable modules. He uses a lot of NLP in his everyday work. One of his concerns is that there's a lot of repetition in programming and problem analysis, that often "reinvent the wheel", so his approach is to auto-extract information and convert it into something highly reusable and searchable (accessible).
Bruno's current main focus is on applying category theory to machine learning (and game theory). He's trying to offer a more formal, "categorical" description of computational modules that are used often in machine learning, that can then be used to construct full systems. As I am not that proficient with category theory, the intuition that I got from Bruno's explanations is that they are working on having a formal specification of a specific module that basically tells you what can be plugged into it (either as input or output). In a sense, that is what category theory is concerned about - composition, and they are analysing modules in both supervised and unsupervised learning. Their work is abstract enough so it's not concerned with basis of the domain over which optimization is being done, neither the input/output interfaces.
I raised my concerns with category theory's (and more general, science's) ability to fully explain all the processes, and how very often composition and modularity are everything that is being talked about, yet it obviously hasn't solved all the problem, to which Bruno pointed me to this great article. I mentioned holistic approach and the lack of formalism for it, and those points were very well addressed in the article as well. Those arguments and reasoning are familiar to me also from my Death of functions? article.
A few other things that I got from this sesh:
- I should learn Clojure
- I should learn Haskell
- after the talk I went ahead and watched this video - Haskell Tutorial (1h17m); it quickly covers what you'd read in a 300-400pg book on Haskell
- I concluded that I should probably write something practical/meaningful to really get the taste of Haskell; naturally, a web server came to my mind because it combines the need for data structures, async operations, at least some code architecture put in place and a lot of utility functions
- I will probably dig through some Haskell-based Github repos to learn more about common patterns in Haskell programming, rules of thumb etc.
- if I were to start learning some language for proof assistants, Agda is a pretty good first choice, but it's recommended to have some experience with functional languages, and Haskell is then a really good choice for that (plus, Agda is implemented in Haskell)
Both Markus and Bruno are doing really interesting and important work, and they are very friendly and open to discussing ideas. Here's where to reach them:
- Markus' webiste - dacapo.io
- Bruno's website - brunogavranovic.com