Jason Dagit wrote:
I was asserting that Haskell is currently 2 layered. Purely functional vs. IO. They integrate nicely and play well together, but I still think of them as distinct layers. Perhaps this is not fair or confusing though. The paper I cited did indeed use codata to define streams so that something, such as an OS, that needs to process infinite streams of requests can still do so.
For a first take on monads, that's not a bad way of thinking about it. But, once you move beyond first thoughts, monads aren't a special separate layer and thinking of them as such is liable to land you in trouble. Monads really are pure, it's just that they get there by existentializing over impurities.[1]
Perhaps you really do mean only the IO monad and not any others, but then the question becomes: whose IO? The IO monad is well-known to be a sin bin for things people don't know or care enough about. Over time things get added to IO and over time things get broken off into their own monads. So then where is the layer boundary over time? I assert that there's no meaningful place to draw the boundary because there's nothing particularly special about IO that isn't shared by other monads like ST or ACIO.
It'd be nice to have a total core language, but it's not clear how to helpfully represent such things in the type system. One variety of non-totality is the |error| function. We could design our types to say that people can't call it, but the whole purpose of |error| is to raise exceptions (a monadic action) from pure code; so as far as the types are concerned, we already can't do any such things. We can eliminate many instances of those non-totalities by adding in refinement types (a modest proposal), in order to prevent people from passing [] to |head| or |tail|, or passing 0 as the denominator of (/), etc.
But there are other non-totalities, such as _|_ which cannot be captured by such means. In order to capture many instances of _|_ we'd need to have our type represent their depth so that we can do co/induction in order to ensure that the function terminates. While we can capture a surprising level of such detail in Haskell's type system, this is marching off in the direction of dependent types which would be making things more complex rather than simpler. I'm not saying that we shouldn't head there, but it doesn't seem to be addressing the goals you had in mind.
[1] Just like existential types, you can put something in but you can never get it back out again. For inescapable monads like IO and ST, this is why they have the behavior of sucking your whole program into the existential black-hole.
-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
