[Haskell-cafe] Re: Total Functional Programming in Haskell

[wren ng thornton]

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