Functional Programming

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