Blog » Fixing Haskell IO
Posted on 13 Feb 2009 17:26
No, Haskell IO isn't broken; that's just a shameless bid for attention. But the metalanguage commonly used to describe Haskell IO is broken.
Here are a few typical examples of how IO in Haskell is described:
A value of type IO a is an “action” that, when performed, may do some input/output, before delivering a value of type a. (Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, p. 5)
a type IO a denoting actions that when performed may do some IO and then return a value of type a. (Imperative Functional Programming, p. 3)
The key idea is to treat a value of type IO a as a “computation” that, when performed, might perform input and output before delivering a value of type a. (A History of Haskell: Being Lazy With Class, p. 25):
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".
Now consider how one might describe a run-of-the-mill non-IO value: "a value of type T a is … a value of type T a". All definitions are tautologies. By definition. If the SDIOH is a true definition, then IO values are not like other values, and we have a two classes of value in Haskell. If it is not a tautology, then it is not a definition, and we still don't know what an IO value is.
Since it is clearly undesirable to have two different kinds of value, it must be that the SDIOH is in fact not a definition. Then what is an IO value?
Part of the problem with the SDIOH is its use of ambiguous terms. It's impossible to discern exactly what it means by "value" and "computation". But that's only part of the problem. The deeper problem, which is related to the terminological problem, is that the semantic model (for lack of a better term) behind the SDIOH adopts a particular perspective on the semantic operations involved in evaluation that forces us to mix being and doing.
The current idiom portrays an IO value as an agent that dynamically performs some kind of action. The GHC implementation of IO operators express this concretely by modeling IO as a state transformer that acts on the RealWorld. 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.
Fixing this requires a shift in perspective and a more refined elaboration of the mental model we use to think about IO in Haskell. The trick is to reverse the perspective. Instead of viewing the program as an agent that acts on the world, we view the world as an agent that provides an interpretation for program. We refine the model by dividing semantics into two parts: internal semantics encompass the mapping from Haskell expressions to lambda expressions, along with lambda conversion of expressions; the external semantics cover the assignment of an interpretation to the lambda expressions.
For example, we can account for the semantics of '3' as follows: the internal mapping takes the Haskell expression '3' to the lambda expression '_3' (using prefixed _ to mark symbols in the metalanguage). The World in turn interprets the program text, mapping '_3' to the integer of that value. If we wish we can define a World metalanguage. Using a Haskell-like syntax, we say '_3' is interpreted as "Z 3" of type "W Z Int".
This gives us a clear, simple account of the semantics of IO values without any notion of action. An IO a value is just an IO a value; no different than any other kind of value. Semantics comes from interpretation. The internal semantics map non-IO expressions to constant (bound) lambda expressions. To account for IO expressions, we use lambda variables. For example, "getChar" maps to something like $v : IO Char$ (assuming our metalanguage uses : to indicate type). In other words, the internal semantics takes an IO expression to a free variable in the metalanguage. Now free variables range over all values of their type; so the World's interpretation of such a free variable is the set of mappings from the variable to the World values of the World type corresponding to the argument of the IO type (the 'a' in IO 'a'). In other worlds, the set of all possible bindings of $v : IO Char$ to World values of type "World Char"; for getChar, something like "Char 'c'".
The meaning of the program then becomes the set of all possible World interpretations of it. The notion of actors and actions has been completely eliminated. The notion of "value of type IO a" has been replaced by a description of the way IO expressions are interpreted. The SDIOH is replaced by something like:
An expression of type IO a is bound to a free variable in the metalanguage, which is bound to a (World) value of type a in each interpretation of the program
Naturally, for this to work we would need to rework other parts of the metalanguage, and we would want to come up with some kind of metalanguage for referring to World types and values. In particular, we need to complement the definition of IO values with a definition of (non-IO) values:
a expression of type T a is bound to an expression in the metalanguage that contains no free variables …
This definition would have to be refined, but the basic idea is to distinguish between lambda expressions whose Head Normal Forms have a constant binding to World values, and those that are free.
- the role of the lambda calculus as a metalanguage is made explicit
- IO expressions bind to free vars in the lambda metalanguage
- a World metalanguage provides a model for interpretations
- Executing a program means having the World give it an interpretation
Like this entry?