[Haskell-cafe] Monad laws in presence of bottoms
wren ng thornton
wren at freegeek.org
Wed Feb 22 07:53:41 CET 2012
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.
More information about the Haskell-Cafe