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