Functional Programming – Philosophical Difficulties

All the currently competing programming paradigms have serious philosophical problems.

FP probably less than the others but it too has its little share, which I deal with here.

Equality

Haskell programs look beautiful. You just write equations and everything magically just works. What could be a prettier dance between declaration (equations) and imperation (works)?

However the equations of Haskell hide a fundamental problem – equality is undecidable in general. Lets look at this from different angles.

[But first a readability note.  Your browser needs to show you the greek letters beta, eta and lambda here "β η λ" and also bottom sign " ⊥ " which looks like _|_ ]

The computability angle

What this says is that two arbitrary objects cannot be checked for equality.
In particular, if for two functions f and g, the programming system could systematically answer the question: f = g (in math notation) or f == g (in Haskell notation) then the halting problem would be solvable.

More generally, infinite objects cannot be checked for equality.  This includes real numbers, infinite lists etc

The λ-calculus angle

β-reduction is computable, η-abstraction/reduction is not.
This implies that when a programmer makes proofs about his programs using β-η etc there will invariably be eureka-steps that cannot be automated.

Note: To avoid confusion, let us state…

The proof angle

While the programmer (or mathematician in general) may be helped by a proof-assistant, the assistant can never take over.
IOW an uncrossable chasm exists between

• Proof-assistants in which anything can be predicatively stated but not necessarily proved
• Programming languages whose modelling power is distinctly weaker than uncomputable frameworks like predicate-calculus or set-theory.

In short, while the equations that we write in Haskell are beautiful they are denotationally deceptive as compared to the fun of ML or the -> of Erlang/Clean.

Am I saying Haskell should changing its syntax. No.

I am saying the Haskell teachers need to tell their students that the equations are bit of a lie – since Haskell commits to executability, and math in general is not executable, something somewhere needs to give.  In the case of Haskell, its equations cannot go backwards like a mathematician's can.

If the price of executability that Haskell pays in the math realm is half-working equality, there is a similar price to be paid for trying to be an executable denotational semantics. How to define…

Undefined?

One of the cornerstones of denotational semantics is the use of 'undefined' or 'bottom' usually written as ⊥ (_|_ if that does not show).

The idea is that 

• programs in general may loop (crash/hang etc)
• programs can be modelled as functions from input to output
• So then to model crashing programs, the trick is to add a special element ⊥ to the range and make all the points of the domain that crash, go to ⊥ in the denotational model.

So far so good…
Now we find that Haskell is doing such a good job of being a (framework for) denotational semantics that we now need to model ⊥ as well.


So… We need to model undefined. How to define  undefined?




The special Haskell-value undefined can never be the denotational bottom ⊥ , but something midway between the real denotational ⊥ and normal values in the Scott partial order.

What does all this have to do with the practicing programmer? Not much if say you are writing numerical or web apps. But if you are working with programming language semantics then it matters to know.

The fact that ⊥ by definition must exist outside the language, brings up the recent arguments about…

Referential Transparency

There's been a recent spate of discussion on the fact RT especially among FPers is a bit hyped.

In summary, Prof Reddy points out that functional programmers have co-opted the term from philosophers and distorted the original intended meaning:

Functional programmers seem to believe that these "values" exist within the programming language, not outside. In doing this, they differ from both the philosophers and the programming language semanticists.

The overarching question is the one of

Firstclassness

One of the biggest articles of hype in the FP community is the fact that FPLs have first-class data types.  While this is true and it is good, the hyping obscures some important aspects – How do we define first-class-ness?

Generally it is defined something like:
A datatype is firstclass if its values/instances

• Can be passed to functions
• Returned from functions
• Created on the fly
• Stored in data structures

And since this is truer for functions in FPLs than in other languages, the FP aficionados preen about their favourite languages.

However the above definition does not include for example that values should be

• Comparable for equality (in Haskell-speak having an Eq instance)
  and the most basic of all…
• Easily viewable (in Haskell-speak having an Show instance)

Now the FP fans will protest that (as we have seen above) having function equality would be tantamount to solving the halting problem and so is not possible.

Being viewable is similar though not the same.

What these two additional clauses show is that in the case of functions, the goal of first-classness is intrinsically harder than for other data types and not merely a weakness of supposedly half-assed languages