[Zettel feedback] Functor (Yeah, just that)

ctietze

This is a very technical note. A somewhat mathematical, even.

On a meta-level, it's interesting to me because category theory is a field for which I have 0 (zero!) formal knowledge. I only know some practical applications from programming patterns. That makes writing a note among the lines of "WTF is a functor" a permanent work in progress: I can only start with my superficial knowledge and expand on it.

That means I'll be keeping one foot in the realm of the known (programming) and one in the unknown (category theory).

While the realm of the known expands with every article I read, I can make amends to this note. This, in turn, means that malleability of these notes pays off very quickly!

Feedback questions:

• The title is just "Functor". Not sure what to change that to, if at all.

  • I pondered "definition of Functor",
  • or "Functor design pattern" (see 2nd reference in the note) because I'm still ultimately interested in the application for programming, and not category theory per se (at least for now)

• Increasing formality and new technical terms: striking a balance.

  • Since I'm not talking in terms like "show me your monad in the category of endofunctors" to anyone in real life, I'm somewhat worried that I won't be able to work with the formal language alone.
  • I should be able to pick it up when I re-read the notes. But I do notice that there's not much I can "hang" this new department on. One foot is in the known, programming, so I actually make sense of "A functor transforms one category into another category" by looking at the code.
  • I was able to introduce some formal statements like "a functor transforms one category into another category" only after I came up with a paragraph that summarizes it in layman's terms. Maybe that's enough to keep me afloat?

Current state

Here's my current iteration:

# 202304251014 Functor
#functor #category-theory

A functor transforms one category into another category.[#20230428funcpat][] It is a data type that can be mapped over.

In practice, that means a functor allows **transformation of all values** using the `map` function while **keeping the structure unmodified**[#20230428func][]. When you map over a list of 20 items, you will still have a list of 20 items, but their values may be different. 

Functors need to adhere to these laws:

1. **Functors must preserve identity morphisms**[#20230428func][]

    If the `map` function is the identity function, the input and output must be the same. (That means: no built-in changes into the `map` function.)

2. **Functors preserve composition of morphisms**[#20230428func][]

    Using `map` with the result of composing two functions `f ∘ g` should be the same as using `map` with `f` and then `map` with `g`.

    In Swift code, that means: `map { x in foo(bar(x)) } == map(foo).map(bar)` 


[#20230428func]: "Functor" on the Haskell wiki, <https://wiki.haskell.org/Functor>
[#20230428funcpat]: "The Functor Design Pattern", 2012-09-15, <https://www.haskellforall.com/2012/09/the-functor-design-pattern.html>

Iteration 0

For Zettelkasten porn, here's the version from earlier today. It was shorter, without any references, picked up from a conversation:

# 202304251014 Functor
#functor 

A functor is a data type that can be mapped using the `map` function, as long as it abides by two laws:

1. If the `map` function is the identity function, the input and output must be the same. (That means: no built-in changes into the `map` function.)

2. Composability: using `map` with the composition of two functions `f ∘ g` should be the same as using `map` with `f` and then `map` with `g`.

    In code, that means: `map { x in foo(bar(x)) } == map(foo).map(bar)` 

Will

Hi @ctietze, let me be the first to offer some observations about "Functor."
1. 'Version 0' is more concise (less wordy) without losing meaning.
2. 'Version 0' could use the references of the 'Current state.'
3. Functor Design Pattern as a title only covers part of the contents. The zettel is about the "laws" that define a functor in coding.
4. Functor Design Pattern Laws in Coding would be a descriptive title.
5. Including the phrase "in Coding," leaves open the future "in Category Theory."

As a beginning programmer, 'Version 0' is understandable. If someone asked me what functor was, I feel confident I could explain the design pattern laws.

chrisaldrich

Kudos on tackling the subject area, especially on your own. I know from experience it's not as straightforward as it could/should be. I'll refrain from monkeying with the perspective/framing you're coming from with overly dense specifics. As an abstract mathematician I'd break this up into smaller pieces, but for your programming perspective, I can appreciate why you don't.

If you want to delve more deeply into the category theory space but without a graduate level understanding of multiple various areas of abstract mathematics, I'd recommend the following two books which come at the mathematics from a mathematician's viewpoint, but are reasonably easy/intuitive enough for a generalist or a non-mathematician coming at things from a programming perspective (particularly compared to most of the rest of what's on the market):

• Ash, Robert B. A Primer of Abstract Mathematics. 1st ed. Classroom Resource Materials. Washington, D.C.: The Mathematical Association of America, 1998.

  • primarily chapter 1, but the rest of the book is a great primer/bridge to higher abstract math in general)

• Spivak, David I. Category Theory for the Sciences. MIT Press, 2014.

  • Spivak had a free draft prepublication version at https://arxiv.org/abs/1302.6946; There's also an open courseware version of his MIT course with a free .pdf textbook (with a 2013 date, but ostensibly a copy of the final published version from 2014) at https://ocw.mit.edu/courses/18-s996-category-theory-for-scientists-spring-2013/

You'll have to dig around a bit more for them (his website, Twitter threads, etc.), but John Carlos Baez is an excellent expositor of some basic pieces of category theory.

For an interesting framing from a completely non-technical perspective/conceptualization, a friend of mine wrote this short article on category theorist Emily Riehl which may help those approaching the area for the first time: https://hub.jhu.edu/magazine/2021/winter/emily-riehl-category-theory/?ref=dalekeiger.net

One of the things which makes Category Theory difficult for many is that to have multiple, practical/workable (homework or in-book) examples to toy with requires having a reasonably strong grasp of 3-4 or more other areas of mathematics at the graduate level. When reading category theory books, you need to develop the ability to (for example) focus on the algebra examples you might understand while skipping over the analysis, topology, or Lie groups examples you don't (yet) have the experience to plow through. Giving yourself explicit permission to skip the examples you have no clue about will help you get much further much faster.

I haven't maintained it since, but here's a site where I aggregated some category theory resources back in 2015 for some related work I was doing at the time: https://cat.boffosocko.com/course-resources/ I was aiming for basic/beginner resources, but there are likely to be some highly technical ones interspersed as well.

ZettelDistraction

@ctietze :

There are many approaches to category theory per se and category theory and programming. Recent publications on category theory have emphasized concrete examples and applications. Spivak's book mentioned by @chrisaldrich and "An Invitation to Applied Category Theory" by Brendan Fong and David I. Spivak are good choices. For functional programming, there is "Category Theory For Programmers" by Bartosz Milewski, with editions for OCaml and Scala and others under Assets. The earlier chapters of Sheaf Theory through Examples by Daniel Rosiak might be helpful to you. This book is released under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 license. Individual chapters are available for download.

If you would like a taste of current category theory treatments of computability, I recommend some of the videos in the YouTube series of the New York City Category Theory Seminar; in particular, Dusko Pavlovic's axiomatic wiring diagram treatment of categorical computability, which includes among the axioms a wiring diagram interpretation of Kleene's $(S^m_n)$ theorem from classical recursion theory--at least that's how I read it when I saw it. A draft of "Programs as Diagrams" by Dusko Pavlovic is available at dusko. org.

Earlier, standard treatments of the category theory motivated the subject with examples from algebraic topology and related areas, not to mention motivation from category theory itself--an understandable tendency repeated so often that it has led to functional fixedness on what counts as an example--in my view. Functional fixedness is the enemy of category theory.^†

As for your notes, you might want to think of Functors as type casts (and conversely) so that a functor $(F:\mathcal{C}\rightarrow\mathcal{D})$ sends objects and morphisms of type $(\mathcal{C})$ to objects and morphisms of type $(\mathcal{D})$.

Cartesian-closed and monoidal (and comonoidal) categories come up frequently in applications of categories to programming and programming semantics, as do representable functors. It takes a while to develop a feeling for it.^‡ Many authors consider the Yoneda Lemma the most crucial theorem in category theory. Still, the natural equivalence of the category of cartesian-closed categories and cartesian-closed functors with the category of simply-typed lambda calculi and translations was foundational for programming language semantics--not to mention categorical logic. A proof of the equivalence is given in Higher Order Categorical Logic by Lambek and Scott, who consider type theory more fundamental than category theory. As for type theory, I recommend Practical Foundations for Programming Languages (Second Edition) by Robert Harper. Cambridge University Press, 2016.

Every basic categorical notion--and much more--is explained in the comprehensive nLab, though this may be more helpful to mathematicians.

Finally, what is category theory?

Category theory is, in some sense, the study of finitely presented categories.
-- Alex Heller. Remark in conversation.

† Despite the CC BY-SA 4.0 license that applies to everything here, something is bound to be plagiarized--it wouldn't be the first time. In my GitHub, I have examples of simplicial objects that are easy to calculate (in SageMath even) and give you concrete examples of infinity categories...this is a work in progress, which won't be so helpful to a programmer. I also program, though nowhere near your level, so it's less likely to benefit me. I may have to wait for retirement to complete the project.

‡ One well-known mathematician (who sadly succumbed to COVID-19) once said I had a taste for homological algebra, but this is another intellectual adventure I must postpone until retirement. My adviser privately told others that "he's no Eilenberg"--Eilenberg, who developed category theory with MacLane, was my adviser's adviser. An Abel prize winner once told me, "You should be a mathematician." One distinguished professor told another professor I needed to think deeply about some subject for a decade. That other professor told me, "you're fundamentally combinatorial." The combinatorialist, with whom I once published, thought I was more algebraic than combinatorial. But the algebraists thought I was better suited to the computer science department. That was before compliant CPAP therapy--now, I disavow virtually everything before February 8th, 2020, when I began compliant CPAP therapy for severe sleep apnea. It seems to take a lifetime to understand mathematics.