Laws and partial values (was: [Haskell-cafe] mapM_ -> Monoid.Monad.map)

[Thomas Davie]

On 24 Jan 2009, at 10:40, Ryan Ingram wrote:

> On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie <tom.davie at gmail.com>  
> wrote:
>> Isn't the point of bottom that it's the least defined value.   
>> Someone above
>> made the assertion that for left identity to hold, _|_ `mappend` ()  
>> must be
>> _|_.  But, as there is only one value in the Unit type, all values  
>> we have
>> no information about must surely be that value, so this is akin to  
>> saying ()
>> `mappend` () must be (), which our definition gives us.
>
> But _|_ is not ().
>
> For example:
>
> data Nat = Z | S Finite
>
> proveFinite :: Nat -> ()
> proveFinite Z = ()
> proveFinite (S x) = proveFinite x
>
> infinity :: Nat
> infinity = S infinity
>
> somecode x = case proveFinite x of () ->
> something_that_might_rely_on_x_being_finite
> problem = somecode infinity
>
> If you can pretend that the only value of () is (), and ignore _|_,
> you can break invariants.  This becomes even more tricky when you have
> a single-constructor datatype which holds data relevant to the
> typechecker; ignoring _|_ in this case could lead to unsound code.

Your proveFinite function has the wrong type – it should be Nat ->  
Bool, not Nat -> () – after all, you want to be able to distinguish  
between proving it finite, and proving it infinite, don't you (even if  
in reality, you'll never return False).

Bob