Category Theory, Haskell, Concurrency, C++
You may think of Tannakian Reconstruction as an example of redundant encoding. It lets you replace a simple hom-set with a much more complex end that is taken over an entire functor category. Why would anyone want to do it? The answer is simple: composition! Morphisms on the left compose according to the rules of [ ]
Two friends, Alice and Bob, live in the same city, but on the opposite sides of a wide river. Every night, Bob looks at the lights on the other side and tries to guess, which one belongs to Alice. They come up with a clever arrangement: Alice will turn on her lights for 10 minutes [ ]
I was originally attracted to category theory when trying to understand Haskell optics. I was puzzled by the van Laarhoven s functor representations and Kmett s use of Tambara modules. By playing Tetris with the Yoneda lemma I was able to make some progress, attacking more and more esoteric topics. With a group of researcher and students [ ]
Previously: Kan Extensions in Double Categories. In programming, actegories play a central role in optics: lenses, prisms, traversals, etc. To understand actegories, let s start with the definition of a monoidal category. Monoidal Category A monoidal category is a category equipped with a tensor product. A tensor product is a functor . We assume that this [ ]
Previously: Kan extensions in Haskell. In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan extension: we can bend the vertical arrow, replacing it with its horizontal conjoint . In a profunctor equipment, this is just [ ]
Previously: Tabulation Tribulations. If you think of functor composition as a form of multiplication, Kan extensions are an attempt to construct inverses of this multiplication. But unlike multiplication, composition is not symmetric, so we have extensions that attempt to undo precomposition, and lifts that do the same for postcomposition. Furthermore, there rarely is a single [ ]
Previously: Bending, Yanking, and Cartesian Squares in Double Categories. We all know what a graph of a function is: it s a set of pairs , where . Similarly, a graph of a relation is a set of pairs where is related to . A profunctor can be viewed as a proof-relevant relation. So a graph [ ]
Previously: Profunctor Equipment in Haskell. The major advantage of string diagrams is that they provide surprisingly natural language for complex diagram manipulations. The fact that two traditional diagrams are equal can be often described as a permission to bend, yank, or pinch strings in particular ways. They provide visual and often tactile clues to our [ ]
Previously: Profunctor Equipment. To make things more palatable for programmers, I decided to provide a toy implementation of some of the equipments in Haskell. The advantage of this encoding is that it can be verified by the compiler, and I still trust the compiler more than I trust the AI. A more adequate implementation would [ ]
The fundamental premise of category theory is that it s possible to fully capture the nature of objects by describing their interactions with other objects of the same type. Those interactions are encoded using morphisms: arrows between objects. What about categories themselves? We define a category by describing its internals: objects and arrows. But true to [ ]