Wednesday, February 07, 2007

Logical implication in Haskell

Logical implication is a common enough operator, usually written "a => b" for a implies b. Haskell doesn't feature a => operator, it would be a syntax error because that symbol is reserved for class constraints. Both QuickCheck and SmallCheck feature incompatible ==> operators for implication.

But Haskell does provide a boolean implication operator, namely (<=)! Yes, by writing the implication symbol backwards, you get standard forward implication!

5 comments:

Alan said...

Clever. I actually had to go to Hoogle to look up (<=) before I realized that it just less-than-or-equal. I feel a little dumb. It never occurred to me that Bool is an instance of Ord.

Edsko said...

It's not *really* implication though because it is too strict in the second argument. (False <= undefined) == undefined, but if we define implies p q = not p || q, then False `implies` q == True. (Though it can possibly be argued that this is a bug in the implementation of <=).

Neil Mitchell said...

Edsko: Very good point, I totally forgot about _|_. And I guess this could be seen as a bug in <=, but it is a fairly reasonable one I guess.

Jan said...

IMHO using this is a bad idea. If you are mathematically inclined (reading a Haskell blog proves you are), then you interpret "a <= b" as a is implied by b, not as a implies b. Your code will confuse a lot of people, especially, if they expect an implication.

Anonymous said...

@Jan: Agree. This is a syntactic misfeature, reminding me of some C-pitfalls. Avoid-checklist of language designers should get one longer due to this.