[Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

Hi Daryoush,

2009/2/13 Daryoush Mehrtash <dmehrtash at gmail.com>

> I have been trying to figure out the distinction between value, function
> and computation.     You raised a few points that I am not sure about.
>
>
> In " "Computation" considered harmful. "Value" not so hot either." you
> said:
>
> I still don't like it; a lambda expression is not a computation, it's a
> formal *representation* of a mathematical object (a *value*).
>
>
> Isn't the lambda expression a representation of  something (potentially
> with recursion) that yields "a value" and not the value itself?   Even
> integer which we think of as values are represented in the same way:
> http://safalra.com/science/lambda-calculus/integer-arithmetic/
>

Excellent question, and it illustrates the problem of "abstraction
management" very nicely.  The way Church presented the lambda operator in
"Introduction to Mathematical Logic" is very instructive.  The basic idea
was how to avoid having to name functions.  This is a very pragmatic
concern; if we didn't have the lambda operator, we would have to invent a
name for every function we want to discuss, which would quickly lead to
unmanageable clutter for both writer and reader.  Church put it in terms
like this:  "x + 2" is a formula, but it doesn't denote anything, since x is
free.  It's not completely devoid of meaning - we get the "+ 2" part - but
it's an "open sentence": not a function, not a value (or: not the name of a
function or value).  But there is a function /associated/ with the formula;
we can denote that function, but only by introducing a name: f x = x + 2.
Now f denotes the function associated with the formula.  Which means we have
two things: syntax, and semantics.  Actually three things, since the name f
is a thing.  The lambda operator just allows us to do the same thing without
names:  the expression "lambda x.x+2" denotes the function associated with
the form x + 2.

So a lambda abstraction expression denotes a function without naming it.
IOW, the function is not the formula; it is an abstract mathematical thing.
A lambda application expression - e.g. (\x -> x + 2)3 denotes application of
the function to an argument.  Here '3' names a "value"; but the value and
the name are distinct.  Lambda calculus thinks of function application in
terms of rewriting forms - it's a calculus, it just manipulates the symbolic
forms.  In other words, the fact that \x -> x + 2 and 3 denote values isn't
important; we say the application denotes 5 because of syntactic rules.  5
is just a symbol that replaces the application expression.

The contrast with ZF set theory helps.  In a set theoretic account,
functions are just sets of ordered pairs.  Application just projects the
second element of the function pair whose first element is equal to the
argument.  The notion of algorithm or computation is totally absent; that's
why ZF is so attractive for semantics.  We only want to know what an
expression means, not how its meaning was discovererd.

So even though lambda calculus may used to describe the symbolic
manipulations needed to find the value of an application, it is not accurate
to say that a lambda expression represents a computation or something that
yields a value, as you put it.  Or at any rate that it /only/ represents a
computation.  It is entirely legitimate to say that "(\x -> x+2)3" denotes 5
(or more accurately, the value represented by the symbol '5'); that
represents the set theoretic perspective.  But lambda calculus licenses us
the think of the same expression as a representation of the reduction chain
leading to the symbol '5'.  So it really depends on your perspective.


>
> In " Fixing Haskell IO" you say:
>
> This "works" well enough; GHC manages to perform IO. But it doesn't fly
>> mathematically. Mathematical objects *never* act, sing, dance, or *do*anything. They just are. A value that acts is an oxymoron.
>>
>
>
> I guess I am not sure what a "mathematical object" is.   Do you consider
> Newton method a mathematical object?   What would be the "value" :
> http://en.wikipedia.org/wiki/Newton's_method#Square_root_of_a_number<http://en.wikipedia.org/wiki/Newton%27s_method#Square_root_of_a_number>
>

Again, it all depends on perspective.  A formal method can be considered a
mathematical object: a sequence.  Just like a lambda expression, viewed as a
representation of a sequence of reductions.  But here again, the
representation and the thing represented are not the same.  Newton's method
is an algorithm, which exists independently of any particular
representation, just like the integer "three" is independent of the symbolic
conventions we use to denote it.   So Newton's method can be considered a
value, just as an algorithm is a kind of value, in the abstract.  And the
function "sqrt" can be considered a value, independent of any algorithm.
Application of Newton's method - note I said "application", not "syntactic
representation of application" can be thought of as a value, or an
algorithmic process, or a piece of syntax, etc.  A syntactic representation
if application can be considered to denote the "final" value, or the process
of computing the value, etc. It all depends on your perspective.

This is a very tricky problem, but it's a writing problem, not a technical
problem, which is what makes it fun for a writer.

>
> Since I have been thinking about Haskell, Monads, etc. I am starting to
> think about the  saying "Life is a journey, not a destination" to imply life
> is a computation not a value.
>

Very nice.  I propose that "Life is a computation, not a value" or some
variant be adopted as the official haskell slogan.  Or maybe something
like:  "Haskell ... because there's more to life than values".

Hope that helps.

-gregg
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090213/04dcc782/attachment-0001.htm