Thomas Davie 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>
> 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
```