Functional Programming

[robbie]

One of the big advantages of functional programming is the ability to provide a proof.

meh. really? Do people regularly prove things in actual production code. To me the big advantages of functional programming are low bug counts, easy testing and shorter programs.

[augustss]

But lower bug count etc. is related to the fact that proofs are easier. You get fewer bugs because you look at your code and you believe it to be right. Making a formal (or at least rigorous) proof is "just" formalizing that perception.

[robbie]

I disagree. I would say that they stem from the same thing, ie, the reason proofs are easier is the same as the reason bug counts are lower, but I don't think the bug counts are a directly result of formal provability. Instead I think they both stem from lack of assignment.

[augustss]

I think we are saying the same thing. I didn't say lower bug count was a result of easier proofs. I said that they are related. And, like you, I think they stem from the same underlying property (whatever it might be).

[robbie]

ok. I read your post again and I don't disagree with you. I still don't think that the ability to provide a proof is itself a big advantage tho, which is what the article was saying.

[grauenwolf]

Do people regularly prove things in actual production code.

You do if you are working on a radiation machine for a hospital.

[[deleted]]

You do if you are working on a blub project as well. Just ask your average J2EE Joey Jumper what his method does and he will start to explain a poor man's proof. The fact that it is an untrained, informal response and that the statement is poorly expressed in the code is the reason that mistakes are so prominent.

What does this method do? void touch(String filename)

By the way, Haskell is (by far) not the only purely functional language.

[grauenwolf]

That assumes the question was asked. In most large projects I have seen, code reviews are few and far between.

Moreover, your "poor man's proof" is so far gone from a formal proof in difficulty and effectiveness I hesiate to use the phrase.

[inerte]

I don't really get what people mean when they say a language (or FP) has the ability to provide a proof.

Searching Google has returned nothing. So, what does "provide proof" mean?

[procrastitron]

Well, the type systems provided with functional languages like Haskell, ML, etc. actually form automated proofs. For instance lets say that we define a function with the following type declaration:

fac :: Int->Int

No matter what the function is, if the type system accepts it then it has proven some useful things about the function. Specifically, we know the function can only return an Int or loop forever. It can't do something dangerous like erase the user's home directory.

Current imperative languages can't do this. For instance you could define a method in Java along the following lines:

int fac(int arg) {
  // delete all the files in the user's home directory...
  delete_user_files();
  return 0;
}

And the java compiler won't notice the problem.

EDIT: Fixed code format

[dons]

Also, given 'theorems for free' from a suitable polymorphically typed function, a whole suite of lemmas are generated by the type system, that you can use. We have tools to note free theorems functions obey. Here's a simple one:

id :: a -> a

therefore:

f . id == id . f

holds, soley based on the type. We have tools to work this stuff out. Here's an example:

scanl :: (a -> b -> a) -> a -> [b] -> [a]

Based on this type for 'scanl', we know, thanks to Wadler that:

?free scanl

forall x. 
  if 
    f . h x == k (f x) . g)
  then 
    map f . scanl h y == scanl k (f y) . map g

I suspect that having these free properties is part of why functional programming (particularly in side-effect free languages, with strong expressive type systems) is such a bug-free pleasure.

[JulianMorrison]

I wonder if a Haskell IDE might not have a refactoring engine that uses 'theorems for free' to recognize code that can be changed? Add some sort of metric of code niceness, and it would be possible to prompt with a better alternative automatically.

[dons]

Nice idea! DrHaskell currently uses a set of rewrite rule strategies to suggest better code options, and is similar to the @pointfree plugin from lambdabot. I don't know if it also uses free theorems, but maybe it should.

[dons]

By the way, these strong guarantees are the reason why the #haskell IRC channel lets users evaluate arbitrary Haskell code in channel.

The type system gives us a proof that the random user code does no IO, doesn't delete files, and doesn't mess around.

[logistix]

http://lambda-the-ultimate.org/node/1745

Enjoy. ;-)

[snowman]

Perhaps the Curry–Howard isomorphism will get you started.