22
$\begingroup$

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?

Improve this question
$\endgroup$
1

2 Answers 2

Reset to default
15
$\begingroup$

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.

Improve this answer
$\endgroup$
26
  • 2
    $\begingroup$ 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. $\endgroup$
    – Dave Clarke
    Feb 15, 2013 at 20:54
  • 5
    $\begingroup$ @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! $\endgroup$
    – Uday Reddy
    Feb 15, 2013 at 22:07
  • 4
    $\begingroup$ @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. $\endgroup$
    – Uday Reddy
    Feb 15, 2013 at 22:14
  • 1
    $\begingroup$ +1 This is really interesting. Do you know any reference that discusses these issues further? $\endgroup$
    – Kaveh
    Feb 16, 2013 at 6:39
  • 3
    $\begingroup$ @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? $\endgroup$
    – Martin Berger
    Feb 16, 2013 at 13:46
10
$\begingroup$

[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!

Improve this answer
$\endgroup$
3
  • $\begingroup$ @GuyCoder, I think that is good idea. By the way, I think this and that question would be on-topic also for Theoretical Computer Science in case you would prefer to post it there. $\endgroup$
    – Kaveh
    Feb 16, 2013 at 13:58
  • $\begingroup$ After dicussing with Uday, a new question will not be specifically asked for this second answer. :) $\endgroup$
    – Guy Coder
    Feb 16, 2013 at 15:29
  • $\begingroup$ State is relativistic. $\endgroup$
    – Shelby Moore III
    Jan 28, 2018 at 4:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.