Re: [Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

On Sat, Feb 14, 2009 at 9:15 AM, Stuart Cook  wrote:

> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[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.

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[roconnor]

I also recommend reading 
 (mostly because I wrote 
it).  Feel free to improve upon it.


--
Russell O'Connor  
``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.''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

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_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 

Re: [Haskell-cafe] IO semantics and evaluation - summary

[Roman Cheplyaka]

* Daryoush Mehrtash  [2009-02-13 11:31:06-0800]
> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[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/

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
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] IO semantics and evaluation - summary

[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