I would like to see function value representations in Haskell. I am
familiar with, though do not fully understand, David Lester's argument
about full abstraction. Getting into this in any detail involves
talking about the relative merits of operational and denotational
semantics. The debate certainly goes back to 1972 when
Scott tussled with Wegner at the Courant Symposium. Wegner said that
operational semantics captured all of a language's meaning. Scott said
that it didn't, refering to a proof by Bohm [in Steel's 1966 book]
that there are equivalent lambda forms which are not mutually reducable.
Essentially, the question is "is beta reduction enough to define the
lambda calculus?" I suspect that this is not of interest to most
Haskell listers so I'll try a different tack.
Consider the following thought experiment:
A) we can translate Haskell into pure lambda calculus. We could probably prove
that the translation preserves meaning relative to some mutually agreeable
semantics for Haskell & the lambda calculus.
B) we can then reduce the lambda calculus step by step by brute force,
text based beta reduction. Will David let me display the result of
each beta reduction? I hope so! I recall vaguely a proof in Stoys's
book of the equivalence of the denotational and operational
semantics for the lambda calculus so presumably the "fudge" is
not needed. If we are not allowed to display each step then
probably we can't do computing or maths any more?
C) at each step in B) we can reverse the translation to
produce some variant of the original Haskell in A). We can
probably prove that reverse translation preserves meaning.
Now, the reverse translation will certainly not be syntactically
the same as the original Haskell but it will be related to it
closely enough to enable a human to see how reduction err evaluation
err execution is progressing.
B) and C) are essentially what functional language implementors do when they
debug their systems by dumping out the internal data structures in some readable
form which they can then relate to the original program. Of course, this depends
on the internal representation. Debugging SK combinators is truly
ghastly! But with super-combinators, the internal form is pleasingly
close to the original code and so relatively easy to reverse engineer.
Similarly, reconstructing lambda calculus from SECD machine configurations
is straightforward.
If we can establish that printable function representations are not
heretical :-) would other people find them useful?
Greg Michaelson
