[Haskell-cafe] Monad laws in presence of bottoms

[wren ng thornton]

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