Last week I attended a Category Theory meetup, and as usual, it looks like "standard" notations were chosen to be maximally confusing. And then there's implicit lifting everywhere. 1/n
It's often important to distinguish an "internal" A⇒B in a category from an "external" A→B in its meta-category… that itself somehow has all arrows internal. Indeed many theorems actually relate arrows at many different levels, which the baroque notations maximally obfuscate.
-
-
Category theory notation starts and stops magic implicit lifting at random, forcing everyone to have complex type and kind inference—that even top specialists sometimes admit to get wrong. Instead of either magic or painful explicit lifting, use quasiquotation and escape!
Show this thread -
In computer science, eval and apply mean very distinct things, but of course, category theorists call "eval" what everyone else calls "apply" (yet correctly call "partial application" by its name). Category theorists? More like Category Terrorists!
Show this thread -
Internal (first-class) functions vs their semantics as external functions; relationship between theory and meta-theory; quotation and (lack of proper) quasiquotation; eval and apply... Category Theorists are just reinventing Lisp, badly, except with ((heavily) dependent) types.
Show this thread -
Category theorists should seriously learn some Lisp. And Conversely, lispers should learn themselves some dependent types.
Show this thread -
Introductions to CT make you believe it's all about preserving the compositional structure of nodes and arrows, but actually, it's about preserving the compositional structure of arbitrarily complex diagrams over increasingly many nested levels of nodes and arrows.
Show this thread -
Category Theory is complex enough that you need all the help you can to understand it, but Category Terrorists invent notation that is maximally confusing with what Mathematicians use, what Computer Scientists use, what Logicians use, and what other Category Terrorists use.
Show this thread -
Some day, I'll understand enough Category Theory to do my own variant with blackjack and hookers—and some coherent notation. And either all the arrows will go from right to left, or function application will be postfix by default.
Show this thread -
The most elementary result of Category Theory, Yoneda's Lemma, requires three levels of arrows, relating internal arrows to external ones that preserve two levels of arrows. Nothing is interesting below three levels: 1. Morphisms, 2. Functors, 3. Natural Transformations.
Show this thread -
There seems to be no convention for diagrams over multiple levels of arrows. Wikipedia's page for the Yoneda Lemma has a semi-nice one with one square inside another, but only position relates two levels, and for more complex diagrams, you'll need at least a third dimension.
Show this thread
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!