On Tue, Oct 25, 2011 at 11:58:37AM +0000, Costello, Roger L. wrote:

Hi Folks,

Are these statements accurate:

I'll give it a shot, hopefully others can chime in with corrections or alternative points of view.

1. The Haskell language is a layer of abstraction on top of Lambda Calculus.

There are a great many different lambda calculi. Haskell (with the exception of IO) can be seen as a layer of abstraction on top of a particular lambda calculus variant known as System F-omega [1] (extended with a fixpoint primitive and various primitive types). In particular, System F omega is a typed lambda calculus with explicit lambdas and applications for *types* (i.e. polymorphism) as well as allowing type operators (i.e. higher kinds). [1] http://en.wikipedia.org/wiki/System_F

2. Haskell programs may be expressed entirely using Lambda expressions.

If you stick to Haskell 98/2010 without IO, this is essentially true. In fact the Haskell Report specifies what amount to translations from various Haskell syntax constructs into System F_omega. Once you add various extensions like GADTs and type families you need something beyond F_omega, but it is still based on a variant lambda calculus.

3. The non-Lambda stuff in Haskell is syntactic sugar to make Haskell programs easier to write.

More or less, yes. See the answer to #2.

4. The field of Lambda Calculus is formal and rich and enables powerful properties of Lambda expressions to be proven.

It is true that all sorts of lambda calculi have been studied in great depth. The field is indeed formal and rich. Usually, though, the focus is on proving properties of entire *systems* (e.g. there are no infinite reductions, they are type-safe, etc.) rather than of individual expressions. One interesting counterexample, however, is the study of *parametricity* (a property of an entire system, including F-omega) which can also be used to prove things about individual expressions (e.g. any expression of type forall a. [a] -> [a] commutes with 'map g' for any function g, that is, it can only rearrange elements of the list, and it must do so in the same way every tiem, regardless of the list contents).

5. A Haskell program may be translated to consist entirely of Lambda expressions. Then, Lambda Calculus may be employed to prove powerful properties about the program.

I don't think it's necessary to translate into F_omega before proving properties of your program. Actually, I think this would be counterproductive. There is already a large body of literature devoted to proving things about Haskell programs directly. -Brent