12
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ In so far as computer science itself is a branch of mathematics... yes $\endgroup$
    – Mariano Suárez-Álvarez
    Commented Jan 15, 2010 at 20:35
  • 3
    $\begingroup$ Wow, my comments are controversial as of late! For context, this was a reaction to Hans Stricker's suggestion that we should find another name for "functional programming" just because it's a computer science term. However, my earlier question "Anything wrong with 'functional programming' besides the fact that it's a computer science term?" is essentially the same as yours. This was an honest question, I do not have a definite opinion about that. $\endgroup$
    – François G. Dorais
    Commented Jan 15, 2010 at 21:23

3 Answers 3

Reset to default
10
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ "Bubble sort and merge sort are the same function under the lens of beta-eta equality" - Not so fast! Even after you have figured out the right algebraic treatment of program state, and have proved that both will give the same outputs on every input, you will still only have proven propositional equality: beta-eta equality is normally something else in intensional type theory. $\endgroup$
    – Charles Stewart
    Commented Jan 16, 2010 at 14:24
  • $\begingroup$ The same function can have wildly (eg, arbitrary towers of exponentials) different runtimes under different evaluation orders. Since even intensional MLTT is consistent with any evaluation order, I don't think the operational properties of purely functional programs have a type-theoretic/logical reading, yet. $\endgroup$
    – Neel Krishnaswami
    Commented Jan 16, 2010 at 15:48
  • $\begingroup$ You can have a monad that specifies the intended computational meaning of a function. Then regular functions of the lambda calculus become denotationally determined, operationally underspecified programs. I'd be surprised, though, if you could fix things so that bubblesort and mergesort are both computational realisations of some underdetermined lambda expression. $\endgroup$
    – Charles Stewart
    Commented Jan 19, 2010 at 9:38
  • $\begingroup$ If you use an omega-rule for list elimination, then bubble sort and merge sort will have the same canonical form. (The necessary infinitary syntax can be represented either in a higher-order fashion, the way Noam Zeilberger does it, or coinductively, the way Girard does in Ludics.) $\endgroup$
    – Neel Krishnaswami
    Commented Jan 19, 2010 at 11:12
  • $\begingroup$ Omega rules aren't syntax! I'm not sure whether they can be functional programming, either. Can you give me a ref (Zeilberger is less taxing than Girard): I'd like to think this through for myself. $\endgroup$
    – Charles Stewart
    Commented Jan 20, 2010 at 9:14
3
$\begingroup$

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).

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ The theory of the untyped lambda calculus is much, much richer than the simply-typed case, and is actually why Scott invented domain theory. Giving a model for it requires finding a category where the isomorphism $D == D -> D$ holds non-trivially, which is a pretty bold thing to imagine. (In fact, Scott wrote a paper arguing against the untyped lambda calculus, on the grounds that there was no way anyone could come up with such a model, shortly before he came up with one!) $\endgroup$
    – Neel Krishnaswami
    Commented Jan 19, 2010 at 9:37
  • $\begingroup$ Scott's model of PCF terms as "simply typed lambda expressions of infinite type" was a work of truly incredible vision, but its result was only to add non-normalizing terms to the simply typed lambda calculus, and the result was still a cartesian closed category. The $D_\infty$ construction does not allow for the sort of blatantly ill-typed terms like (4+"Fred") that are allowed in LISP, Python, Ruby -- nor should it!. $\endgroup$
    – Adam
    Commented Jan 19, 2010 at 20:16
  • 2
    $\begingroup$ Er, sure it does. You just take the universal domain to be a coalesced sum including an error case, and blatantly ill-typed stuff denotes the error value. The error is conventionally called Wrong, which is where the "wrong" in the phrase "well-typed programs don't go wrong" comes from. $\endgroup$
    – Neel Krishnaswami
    Commented Jan 19, 2010 at 23:32
2
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This being the mostly categorical theory arising out of Moggi's computational lambda calculus and its applications. $\endgroup$
    – Charles Stewart
    Commented Jan 16, 2010 at 2:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .