[Haskell-beginners] Are these statements about Haskell correct?

[Brent Yorgey]

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