Laws and partial values (was: [Haskell-cafe] mapM_ ->
tom.davie at gmail.com
Sat Jan 24 04:47:32 EST 2009
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>
>> 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 () ->
> 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).
More information about the Haskell-Cafe