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

Jon Fairbairn jon.fairbairn at cl.cam.ac.uk
Sun May 23 04:35:32 EDT 2010

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)

More information about the Haskell-Cafe mailing list