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