[Haskell-cafe] Re: Proof question -- (==) over Bool

[Jon Fairbairn]

Alexander Solla <ajs at 2piix.com> writes:

> On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
>
>> Since Bool is a type, and all Haskell types include ⊥, you need
>> to add conditions in your proofs to exclude it.
>
> Not really.  Bottom isn't a value, so much as an expression
> for computations that don't refer to "real" values.  It's
> close enough to  be treated as a value in many contexts, but
> this isn't one of them.

It seems to me relevant here, because one of the uses to which
one might put the symmetry rule is to replace an expression “e1
== e2” with “e2 == e1”, which can turn a programme that
terminates into a programme that does not.

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk
http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html  (updated 2009-01-31)