23

In reading Uday Reddy's answer to What is the relation between functors in SML and Category theory? Uday states

Category theory doesn't yet know how to deal with higher-order functions. Some day, it will.

As I thought Category theory was able to serve as a foundation for math, then it should be possible to derive all of math and higher-order functions.

So, what is meant by Category theory doesn't yet know how to deal with higher-order functions? Is it valid to consider Category theory as a foundation for math?

Community
  • 1
Guy Coder
  • 5,231
  • 3
  • 31
  • 67

2 Answers2

15

The issue with higher-order functions is simple enough to state.

  • A type-constructor like $T(X) = [X \to X]$ is not a functor. It should have been.

  • A polymorphic function like ${\it twice}_X : T(X) \to T(X) = \lambda f.\, f \circ f$ is not a natural transformation. It should have been.

If you read Eilenberg and MacLane's original category theory paper, (PDF) the intuitions they present cover those cases. But their theory doesn't. Theirs was a great paper for 1945! But, today, we need more.

The reaction of category theorists to these issues is a bit perplexing. They act as if higher-order operations form a Computer Science idea; they are of no consequence to mathematics. If that is so, then a foundation of mathematics would not be good enough for a foundation of computer science.

But I don't seriously believe that. I believe that higher-order functions would be quite important for mathematics as well. But they have not been seriously explored. I am hopeful that, some day, they will be explored and the limitations of category theory will be realized.

Guy Coder
  • 5,231
  • 3
  • 31
  • 67
Uday Reddy
  • 4,402
  • 1
  • 20
  • 24
  • 2
    It's amazing that they don't consider higher-order functions interesting, considering the depths they go when exploring higher-dimensional algebra, n-category theory and the like. Comparatively, higher order functions seem so down-to-earth. Especially, if that earth involves Haskell programs. – Dave Clarke Feb 15 '13 at 20:54
  • 5
    @DaveClarke. I think what they would like to see is a compelling example like the one Eilenberg and MacLane start with. All $n$-dimensional vector spaces are isomorphic to each other. So, a vector space is isomorphic to its own dual: $A \cong A^*$. However, these isomorphisms are not "natural". (They use particular bases - "representation-dependent" in our speak.) On the other hand the isomorphism $A \cong A^{**}$ is "natural", works the same way for all bases. To ask for a Category Theory 2.0, we need a similar killer example! – Uday Reddy Feb 15 '13 at 22:07
  • 4
    @DaveClarke. What happens in normal mathematics is that mathematicians very cleverly reduce higher-order things to first-order structures. For instance, the type $T(X)$ I gave above is just a monoid, whose multiplication is a first-order operation. If you recall your Linear Algebra, the linear transformations $A \to B$ are turned into a vector space, and then all its operations become first-order. Automata theory (Computer Science again) might have been the first place where this trick did not work. If Eilenberg had another 10 years of active life, he might have got on to the problem. – Uday Reddy Feb 15 '13 at 22:14
  • You've caught my interest too. – Dave Clarke Feb 16 '13 at 07:22
  • @Kaveh: There is plenty of literature on the subject. But very few people would put things in such strong terms as I do, for fear of offending category theorists. So, you have to read between the lines to see what they are really saying! – Uday Reddy Feb 16 '13 at 10:26
  • 5
    $T(X) = [X \to X]$ is a functor in a category of section-retraction pairs. – Andrej Bauer Feb 16 '13 at 12:39
  • 4
    @UdayReddy Arguably, there is a clever first-orderisation of higher-order functions, namely R. Milner's Functions as processes, which translates $\lambda$-calculus into $\pi$-calculus. The game-theoretic first-orderisations of functions are variants of Milner's idea. Of course $\pi$-calculus is not itself playing nicely with current, category theoretic notions of homomorphism. So today, when we compare processes, we generally use variants of bisimulations as tools. Maybe that's no coincidence? – Martin Berger Feb 16 '13 at 13:46
  • 1
    I thought mathematics treated higher-order functions under the name of functionals. In statistics, I encountered Gâteaux derivatives. – Raphael Feb 16 '13 at 14:58
  • 1
    @Raphael. Indeed, there are plenty of places where higher-order functions pop up in mathematics. It will be great if any of them can lead to an example of a useful higher-order polymorphic function, which fails to be "natural" by the Eilenberg-MacLane definition. – Uday Reddy Feb 16 '13 at 15:32
  • 1
    @AndrejBauer: There is indeed some connection between "algebraically compact" categories and parametricity, which slips my mind now. But I would hold that the problems of mixed variance are more general, which should be dealt with even before we consider diverging elements. – Uday Reddy Feb 16 '13 at 19:09
  • @MartinBerger: Indeed, the apparent "first-orderness" of $\pi$-calculus is thus deceptive. The same kind of issues arise in dealing with simple imperative programs and finite state automata as well, as I mention in my second answer. – Uday Reddy Feb 16 '13 at 19:14
  • 1
    @UdayReddy I don't understand your answer. What makes $\pi$-calculus non first-order? – Martin Berger Feb 16 '13 at 20:37
  • 2
    The section-retraction pairs are not just about algebraic compactness or divergence. They also take care of mixed variance by having morphisms which "go in both directions". And I never said "algebraically compact", actually. – Andrej Bauer Feb 16 '13 at 23:26
  • @AndrejBauer. Ok, fair enough. Do these categories with section-retraction pairs allow one to treat, for instance, ${\it twice}_X$ as a natural transformation? – Uday Reddy Feb 16 '13 at 23:32
  • @MartinBerger. I wish I knew. You are the $\pi$-calculus expert! My feeling is that whenever we deal with state, we have state transformation functions whose type is like $T(X)$ -- where $X$ represents the state set. So, dealing with state is inherently higher-order. – Uday Reddy Feb 16 '13 at 23:37
  • @UdayReddy I'm not sure. Depends what you mean by higher-order. State transformation functions are one specific way of understanding stateful languages, but surely not the only one. – Martin Berger Feb 17 '13 at 12:22
  • @MartinBerger. "Higher-order" has the effect that the type $T(X)$ has both covariant and contra-variant occurrences of $X$. My feeling is that that kind of mixed variance remains no matter what formalism you use to represent the phenomena. That is my explanation in any case. If the present theory of $\pi$-calculus is unable to explain why homomorphisms are not enough to compare processes, then it seems that that is a question for the $\pi$-calculus experts to think about! – Uday Reddy Feb 18 '13 at 08:13
  • @UdayReddy There isn't just one translation of $T(X) = X \rightarrow X$, e.g. CBV, CBN, ... If you look at the standard CBV translation, you get $(\alpha \rightarrow \beta)^{\bullet} =((\overline{\alpha^{\bullet}}(\beta^{\bullet})^{\uparrow})^{!})^{\uparrow}$ where $\overline{\alpha^{\bullet}}$ is the dualisation of the translation $\alpha^{\bullet}$. Dualisation simply means exchanging input for output and vice versa. So yes, you keep mixed variance. I don't know if homomorphisms are enough, because there is no good notion of homomorphism in the sense of categories in process theory. – Martin Berger Feb 18 '13 at 08:59
  • @UdayReddy I believe that this is because categorical composition is too restricted to give a good account of process composition. However, if we restrict our attention to very specific processes such as the translation of e.g. typed $\lambda$-calculi, it might be possible to investigate what generalisation of the concepts of functor and natural transformation are required, so that type constructors like $((\overline{\alpha^{\bullet}}(\beta^{\bullet})^{\uparrow})^{!})^{\uparrow}$ have nice, abstract properties. It's an interesting question. – Martin Berger Feb 18 '13 at 09:08
  • @MartinBerger. Sorry, I didn't mean that you need to encode $T(X)$ in anything. My meaning was that a type such as $T(X)$ is involved in the guts of of any state-manipulating mechanism, including the $\pi$-calculus. That is likely to be the reason why you need bisimulation relations rather than homomorphisms to compare processes. (This issue is not resolved by encoding something in $\pi$-calculus.) – Uday Reddy Feb 19 '13 at 17:28
  • @UdayReddy That may well be the case, but doesn't it show that the issue is not higher-orderness, since the $\pi$-calculus isn't, but rather something else? – Martin Berger Feb 19 '13 at 18:29
  • Yes, from your point of view, the issue is mixed variance. – Uday Reddy Feb 19 '13 at 19:43
  • @UdayReddy Something just occurred to me, but it's far from well-though out: although Milner, and many following his lead, have translated higher-order functions into calculi like $\pi$ that are, prima facie, first order, Milner's encoding is really 'just' an encoding up to strong bisimulation (IIRC). It might be the case, but this would have to be checked more thoroughly, that higher-orderness sneaks back in through this quotienting. – Martin Berger Mar 07 '13 at 16:16
  • @MartinBerger. As I said previously, I believe that $\pi$ calculus is "higher-order" on its own. No need to encode anything. Humble finite automata are already "higher-order". See the paper on "Products of Automata" that I mentioned in my second answer, written way back in 1963! Basic imperative programs are "higher-order". That is what Milner's 1968 paper shows. Apparently, you can't do anything stateful without being higher-order. Quite amazing! – Uday Reddy Mar 07 '13 at 22:29
  • @UdayReddy I know you've been saying this. What I'm trying to find out is if it's true! ;-) To do this, it would be helpful to formalise the notions first/higher-order at play here. – Martin Berger Mar 11 '13 at 13:57
  • 2
    This is ill-informed at best. Categorical semantics of lambda-calculus has been around since (at least) the '80s, thus including all the HO functions you want. There's also very standard notions of functoriality and naturality that apply to the examples you give, look up profunctors and dinaturality, as well as all lit on semantics of parametricity. You know, some things happened since 1945. – mattecapu Jul 15 '24 at 06:42
13

[This second answer presents an outline of what a "Category Theory 2.0", that deals with higher-order functions properly, might look like.]

We have known for a long time how to deal with higher-order functions in reasoning about them.

  • When an algebraic structure has higher-order operations, homomorphisms don't work. We must use logical relations instead. In other words, we must move from "functions preserving structure" to "relations preserving structure".

  • To talk about "uniform" or "simultaneously given" transformations on higher-order types, naturality doesn't work. We must use relational parametricity instead. In other words, we must move from "families preserving all morphisms" to "families preserving all logical relations".

  • Composition of logical relations is of no consequence. The $\to$ type constructor doesn't preserve their composition, and nothing depends on it. (This observation is at logger heads with the category theorists' belief that composition is fundamental!)

A quick introduction to these issues is in Peter O'Hearn's section on "Relational Parametricity" in Domains and Denotational Semantics: History, Accomplishments and Open Problems (CiteSeerX).

I might also add that reasoning about state is where higher-order functions show up prominently. Automata-theorists were the first to recognize that homomorphisms don't work correctly, in a historic paper called Products of Automata and the Problem of Covering. They used terms like "weak homomorphisms" and "covering relations" to refer to logical relations. In due course, terms like "simulation" and "bisimulation" were used to refer to them. Davide Sangiorgi's survey article: On the Origins of Bisimulation and Coinduction covers all of this early history and more.

The need for relational reasoning repeatedly crops up in reasoning about state, in particular imperative programming. Very few people notice that the humble "semicolon" is a higher-order operation. So, you cannot get off the ground in thinking about imperative programs without knowing how to deal with higher-order functions. We keep ignoring the issues of state and imperative programming in the mistaken belief that mathematics has all the answers. So, if mathematicians don't understand state, it must be no good! Nothing could be further from the truth. State is at the heart of Computer Science. We will be advancing science in general by showing people how to deal with state!

Guy Coder
  • 5,231
  • 3
  • 31
  • 67
Uday Reddy
  • 4,402
  • 1
  • 20
  • 24