Many thanks to everybody who tried to set me straight on the thread about IO monad and evaluation semantics. I've begun summarizing the info, and I believe I've come up with a much better way of explaining IO; just flip the semantic perspective, and think in terms of interpretations instead of actions. Voila! Oxymoron (values that perform actions) eliminated. See the "Computation considered harmful" and "Fixing Haskell IO" articles at http://syntax.wikidot.com/blog Naturally I would be grateful for any corrections/comments. Thanks, gregg
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/ 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
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.
daryoush
2009/2/13 Gregg Reynolds
Many thanks to everybody who tried to set me straight on the thread about IO monad and evaluation semantics. I've begun summarizing the info, and I believe I've come up with a much better way of explaining IO; just flip the semantic perspective, and think in terms of interpretations instead of actions. Voila! Oxymoron (values that perform actions) eliminated. See the "Computation considered harmful" and "Fixing Haskell IO" articles at http://syntax.wikidot.com/blog
Naturally I would be grateful for any corrections/comments.
Thanks,
gregg
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
* Daryoush Mehrtash
Isn't the lambda expression a representation of something (potentially with recursion) that yields "a value" and not the value itself?
The same terms may refer to different notions. If you think of values as mathematical objects, they are denotation of syntactic constructs (value 1 is denotation of "1", as well as of "(\x -> x-2) 3"). However, in operational (rather than denotational) semantics, "1" is value (result of evaluation; normal form) of "(\x -> x-2) 3", and is itself a syntactic construct. So, you really need to define (and understand) your terms before talking about them.
Even integer which we think of as values are represented in the same way: http://safalra.com/science/lambda-calculus/integer-arithmetic/
Church numerals are introduced in _untyped_ lambda calculus, while we are probably talking about _typed_ lambda calculus (as implemented in Haskell). In the later integers usually are introduced as a basic type. -- Roman I. Cheplyaka :: http://ro-che.info/ "Don't let school get in the way of your education." - Mark Twain
Hi Daryoush,
2009/2/13 Daryoush Mehrtash
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_numberhttp://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
I also recommend reading http://www.haskell.org/haskellwiki/IO_Semantics (mostly because I wrote it). Feel free to improve upon it. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''
From "Fixing Haskell IO": We can summarize the SDIOH (Standard Definition of IO in Haskell) as "a value of type IO a is a value, that performs, then delivers a value of type a".
I think you've already made a critical mistake here. The quotes you give all describe an IO value as something that "when performed" results in input/output, whereas your summary describes it as something "that performs". The original quotations suggest that some outside agent interprets the values and performs the actions they denote, whereas it is your summary that has made the linguistic shift to values that dance about on tables of their own accord. In my mind, Haskell programs never actually "do" anything. Instead they merely denote a value of type IO () that consists of tokens representing input/output primitives, glued together by pure functions. It is the job of the runtime to take that value and actually modify the world in the manner described by the program. Stuart
On Sat, Feb 14, 2009 at 9:15 AM, Stuart Cook
From "Fixing Haskell IO":
We can summarize the SDIOH (Standard Definition of IO in Haskell) as "a value of type IO a is a value, that performs, then delivers a value of type a".
I think you've already made a critical mistake here. The quotes you give all describe an IO value as something that "when performed" results in input/output, whereas your summary describes it as something "that performs". The original quotations suggest that some
outside agent interprets the values and performs the actions they
denote, whereas it is your summary that has made the linguistic shift to values that dance about on tables of their own accord.
I see you point, and it perfectly illustrates the problem of ambiguity ( http://syntax.wikidot.com/blog:5). "Action" and "Performance" are even more ambiguous than "computation" and "evaluation". The natural analog to the SDIOH is theatrical performance. Where is the action, on the page or on the boards? Who performs the action, the character or the thespian? Whose action is it? Even if we settle on these questions, we have to account for "delivers a value". What does the performance of the action of Hamlet deliver? Dead Polonius? Catharsis? In the end it doesn't matter how one interprets "action that is performed"; either way, there must be an agent. No agent, no performance. As you point out, the SDIOH can be read as positing an "outside agent"; it can also be read to posit the value itself as performer (which must interact with an outside agent). All of which leads to the very interesting philosophical question of what a program process actually //is//: an agent acting on a computer, or a script for the computer to enact (qua agent/thespian). Either way the SDIOH effectively tries to incorporate action/agency into the formal semantics. My proposition is just that we avoid the whole mess by eliminating notions like action, performance, and delivery. Split the semantics into internal (standard denotational stuff) and external (interpretation, which can also be represented mathematically), and you get a clearer, cleaner, simpler picture with no philosophical complications. I'm working on some diagrams and simpler language; once I'm done I guess I'll find out.
In my mind, Haskell programs never actually "do" anything. Instead they merely denote a value of type IO () that consists of tokens representing input/output primitives, glued together by pure functions. It is the job of the runtime to take that value and actually modify the world in the manner described by the program.
I wouldn't try to talk you out of whatever works for you. Just scratching a rather persistent itch about clear, simple, formal, complete representations of the intersection of math and the world. Thanks, gregg
participants (5)
-
Daryoush Mehrtash -
Gregg Reynolds -
roconnor＠theorem.ca -
Roman Cheplyaka -
Stuart Cook