On 24 Jan 2009, at 10:40, Ryan Ingram wrote:
On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie <[email protected]>
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_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
