2009/2/13 Daryoush Mehrtash <dmehrtash@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

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