On 10 Feb 2009, at 12:24 am, Gregg Reynolds wrote:
My bad, I restate: a value cannot be both static and dynamic.
It's not clear what you mean here, but in what sense are "static" values not a subset of "dynamic" ones?
Or an object and a morphism.
Crack open any book on category theory and you will discover that an object CAN be a morphism. Not only can the morphisms of one category be objects of another, but you can build a category where the objects and the morphisms are the same things.
Or an element and a function.
An element of _what_? Functions can be elements of sets. Mathematicians routinely deal with function spaces. If you mean that F : S -> S cannot be an element of S, then if you mean a set theoretic function, no, but a Scott domain *can* contain the continuous functions over itself.
Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction.
False as a generalisation about mathematics. False about functional programming languages, the very essence of which is treating functions ("morphisms") as values ("objects") exactly like any other values.
That doesn't erase the difference between object and morphism.
There is no intrinsic difference between objects and morphisms. It's what you DO with something that makes it an object or a morphism (or both).
If you do erase that difference you end up with mush. getChar / looks/ like an object, but semantically it must be a morphism.
getChar is an element of an abstract data type in Haskell. PERIOD. Since a morphism is characterised by its source and target objects, and since getChar is not so characterised, in what sense is getChar a morphism? *Within Haskell*, getChar is just some value. For all you or I can tell to the contrary, it might be the letter 'G' or a JPEG image of the planet Mars. It's only as part of a whole system of IO primitives in the context of Haskell that the value is interpreted as a description of the "read a character from standard input" action.
But it can't be a function, since it is non-deterministic.
No it isn't. getChar is perfectly deterministic. Whenever you ask for the value of getChar, you get the *same* value. Evaluating getChar does no input whatever. If you compute map (\_ -> getChar) [1..n] you get a list containing n copies of the value of getChar, and NO INPUT WHATSOEVER happens.
So actually the logical contradiction comes from the nature of the beast.
There is no logical contradiction because you have mistaken the nature of the beast.
Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor.
Surely "IO" and "Char" are type constructors, and "Char" and "IO Char" are types.
One would expect getChar to yield a value of type IO Char, no?
Yes, that's EXACTLY what it does. The only thing the expression (getChar) ever gives you is an (abstract) value of type IO Char.
But it delivers a Char instead.
No it doesn't. getChar delivers, always and only, a value of type IO Char. Call that value Gamaliel. When Gamaliel is *performed* by the Haskell environment, *then* a character is read (the action) and returned. But it's Gamaliel that delivers a Char, not getChar.
This is way confusing.
Composer (Haskell program) writes score (computes getChar). Performer (Haskell environment) sings score (performs Gamaliel). Sound happens (a character is read).
So I take "type IO foo" to mean "type foo, after a side effect".
No. Mistake not: there COULD be a type system not unlike that. Look up "effect systems". Haskell's is not one of them. By the way, (return 'x') has type IO Char, but never has any side effects. Type "IO foo" can be usefully read as meaning "descriptions of actions that when carried out also yield a value of type foo".
In a sense "getChar :: IO Char" isn't even a true type signature.
Yes it is. It is exactly and perfectly true. Have you actually read the classic paper "How to declare an imperative", P. Wadler, ACM Computing Surveys 29, 3 (1997). For me, this was more helpful than any tutorial on monads and monadic I/O that I ever read.