>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