DavidA wrote:
Okay, I see. Well that's interesting, because it suggests that your proof might break under modest extensions to the language.
Yes. The free theorem used was a "naive" one, for the simplest possible model of Haskell, not even taking care of possible nontermination and seq. But http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ can produce less naive ones as well. In particular, it can also produce free theorems for types involving class constraints, like Eq or Ord. That would deal with situations where the type variables a and b in the type of fmap were class-constrained, as you suggest. And finally, another plug: explanations for precisely the kind of type-based reasoning I used in the earlier mail can be found in the thesis I advertised today on the general list: http://wwwtcs.inf.tu-dresden.de/~voigt/habil.pdf Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de