[Haskell-cafe] Re: Total Functional Programming in Haskell
wren ng thornton
wren at freegeek.org
Wed Oct 1 19:53:18 EDT 2008
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.
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
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.
 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
More information about the Haskell-Cafe