Is functional programming a branch of mathematics? - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T04:57:24Z http://mathoverflow.net/feeds/question/11916 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/11916/is-functional-programming-a-branch-of-mathematics Is functional programming a branch of mathematics? Charles Stewart 2010-01-15T20:31:13Z 2010-01-18T23:19:56Z <p>In <a href="http://mathoverflow.net/questions/11845/theory-mainly-concerned-with-lambda-calculus/11861#11861" rel="nofollow">Theory mainly concerned with lambda-calculus?</a>, F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics:</p> <blockquote> <p>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. </p> </blockquote> <p>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.</p> <p>Is this true?</p> http://mathoverflow.net/questions/11916/is-functional-programming-a-branch-of-mathematics/11928#11928 Answer by B. Bischof for Is functional programming a branch of mathematics? B. Bischof 2010-01-15T21:45:14Z 2010-01-15T21:45:14Z <p>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.</p> http://mathoverflow.net/questions/11916/is-functional-programming-a-branch-of-mathematics/11976#11976 Answer by Neel Krishnaswami for Is functional programming a branch of mathematics? Neel Krishnaswami 2010-01-16T10:11:38Z 2010-01-16T10:11:38Z <p>So, I'm a computer scientist working in this area, and my sense is the following: </p> <p>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 <em>all</em> the facts about the programming aspects. </p> <p>The reason is that when we look at a lambda-term as a program, we additionally care about its <em>intensional</em> properties (such as space usage and runtime), whereas in mathematics we only care about the <em>extensional</em> 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.</p> <p>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.</p> <p>[*] FYI: Here I'm using "intensional" and "extensional" in a difference sense than is used in Martin-Lof type theory. </p> http://mathoverflow.net/questions/11916/is-functional-programming-a-branch-of-mathematics/12254#12254 Answer by Adam for Is functional programming a branch of mathematics? Adam 2010-01-18T23:19:56Z 2010-01-18T23:19:56Z <p>I think most people here would agree that Category Theory is part of mathematics.</p> <p>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.</p> <p>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).</p>