[Haskell-cafe] Monad laws in presence of bottoms

[wren ng thornton]

On 2/21/12 2:17 AM, Roman Cheplyaka wrote:
> * Sebastian Fischer<fischer at nii.ac.jp>  [2012-02-21 00:28:13+0100]
>> On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka<roma at ro-che.info>  wrote:
>>
>>> Is there any other interpretation in which the Reader monad obeys the
>>> laws?
>>
>>
>> If "selective strictness" (the  seq  combinator) would exclude function
>> types, the difference between  undefined  and  \_ ->  undefined  could not
>> be observed. This reminds me of the different language levels used by the
>> free theorem generator [1] and the discussions whether  seq  should have a
>> type-class constraint..
>
> It's not just about functions. The same holds for the lazy Writer monad,
> for instance.

That's a similar sort of issue, just about whether undefined == 
(undefined,undefined) or not. If the equality holds then tuples would be 
domain products[1], but domain products do not form domains! In order to 
get a product which does form a domain, we'd need to use the smash 
product[2] instead. Unfortunately we can't have our cake and eat it too 
(unless we get rid of bottom entirely).

Both this issue and the undefined == (\_ -> undefined) issue come down 
to whether we're allowed to eta expand functions or tuples/records. 
While this is a well-studies topic, I don't know that anyone's come up 
with a really pretty answer to the dilemma.


[1] Also a category-theoretic product.

[2] Aka: data SmashProduct a b = SmashProduct !a !b

-- 
Live well,
~wren