On 2/21/12 11:54 AM, Dan Doel wrote:
You don't have to get rid of bottom entirely (I think). If you make matches against products irrefutable, then you're again in the situation of seq being the only thing able to distinguish between _|_ and (_|_, _|_), so we could keep the current implementation (which is efficient) without it being possible to observe within the language. You just have to make seq not be magic on products. Miranda did this, except it still had a seq which exposed the lie.
I thought Miranda identified _|_ with (_|_,_|_) ...though I admit I never really played around with Miranda. In any case, the point is that the weirdness of Haskell's products and function spaces are related around this issue of eta expansion. Haskell's sums are also weird (they're not category-theoretic coproducts), but that's not clearly an issue with eta. When it comes to practical utility, I think the choices Haskell made are quite nice. I'd love for smash products to have built-in syntax like tuples do, so I could use them cleanly rather than doing (((,) $! a) $! b) or defining my own ADT for them; but I understand entirely about why the Haskell committee decided that having two different versions of products/tuples would lead to API bloat and user confusion. However, while Haskell's choices are quite nice from a practical perspective, when it comes to theoretical rigor they're quite ugly. And that's the issue we're running into here when trying to figure out a theoretically sound way of defining how monads should behave with respect to bottoms. -- Live well, ~wren