Just a small addendum to Mark's response to Warren: Overloading (even just polymorphism, as Mark says) does compromise equational reasoning, in much the same way that lexical scoping does. That is x = y |- f x = f y , provided it's the same x and the same y. Cheers, --Joe
