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

[Ryan Ingram]

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.

  -- ryan