Luke Palmer wrote:
I've been wondering, is it ever possible to have two (extensionally) different Functor instances for the same type? I do mean in Haskell; i.e. (,) doesn't count. I've failed to either come up with any examples or prove that they all must be the same using the laws.
For "not-too-exotic" datatypes, in particular for algebraic data types with polynomial structure (no exponentials, embedded function types, and other nasties), I would conjecture that indeed there is always exactly one Functor instance satisfying the identity and composition laws. But for proving this the two equational laws would not be enough. Rather, one would also need to use that fmap must be sufficiently polymorphic. Basically, a proof by a version of free theorems, or equivalently in this case, properties of natural transformations. And no, I don't have a more constructive proof at the moment ;-) Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de