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

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

On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie 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