Is functional programming a branch of mathematics? - MathOverflow

Is functional programming a branch of mathematics?

2010-01-15T20:31:13Z

In Theory mainly concerned with lambda-calculus?, F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics:

That would never stick unless there's another good reason. Besides, the schism between cs and math is very recent, I would contend that "functional programming" is actually a math term, historically speaking. More importantly, it would be wrong to use a term different than those who use it most, namely theoretical computer scientists, who are very competent mathematicians by the way.

The idea, I think, is that the overlap between the kind of constructive mathematics that follows the formulae-as-types correspondence, and pure functional programming is so substantial that the core of the two topics is essentially the same subject.

Is this true?

Answer by B. Bischof for Is functional programming a branch of mathematics?

2010-01-15T21:45:14Z

There is some work in using monoidal category theory in functional programming in languages like Haskell. In addition to simply using the ideas and implementing them, they develop new frameworks for the theory, new applications of the theorems, and presentations of the theory. I say this is a branch of mathematics, but it is a sliding scale depending on how you treat it.

Answer by Neel Krishnaswami for Is functional programming a branch of mathematics?

2010-01-16T10:11:38Z

So, I'm a computer scientist working in this area, and my sense is the following:

You cannot do good work on functional programming if you are ignorant of the logical connection, period. However, while "proofs-as-programs" is a wonderful slogan, which captures a vitally important fact about the large-scale structure of the subject, it doesn't capture all the facts about the programming aspects.

The reason is that when we look at a lambda-term as a program, we additionally care about its intensional properties (such as space usage and runtime), whereas in mathematics we only care about the extensional properties (i.e., the relation it computes).[*] Bubble sort and merge sort are the same function under the lens of $\beta\eta$ equality, but no computer scientist can believe these are the same algorithm.

I hope, of course, that one day these intensional factors will gain logical significance in the same way that the extensional properties already have. But we're not there yet.

[*] FYI: Here I'm using "intensional" and "extensional" in a difference sense than is used in Martin-Lof type theory.

Answer by Adam for Is functional programming a branch of mathematics?

2010-01-18T23:19:56Z

I think most people here would agree that Category Theory is part of mathematics.

The study of strongly-typed functional programming languages is really just the study of cartesian closed categories, so I think that this particular part of functional programming is legitimate mathematics. And Domain Theory is the study of the category of complete partial orders with bottom, so I would include that too.

I don't think I would extend that to untyped or dynamically-typed languages (LISP). Also, I'd probably pick a term other than "functional programming" since subfields of math are rarely named with gerunds ("strongly typed functional languages" is probably the most accurate, but a bit verbose).