Janis Voigtlaender
DavidA wrote:
I suspect that the answer to the question is, yes, you can have different Functor instances. All you need is a sum-product type that it's possible
to
interpret as two different abstractions, leading to two different Functor instances.
The sum-product types are exactly the "not-too-exotic" types to which my proof applies. So as long as extensional equivalence means Haskell equivalence, and not some "modulo an interpretation" equivalence (like considering two lists equivalent if they contain the same elements but in potentially different order), the answer is no, one cannot have different funtor instances.
Ciao, Janis.
Okay, I see. Well that's interesting, because it suggests that your proof might break under modest extensions to the language. The thing that led me to suggest list / set as an example was consideration of Data.Set. Conceptually, this should be a Functor instance - given f :: a -> b, we should be able to derive fmap f :: Data.Set a -> Data.Set b, eg fmap f xs = (fromList . map f . toList) xs However, we can't currently express this in Haskell, because Data.Set requires Ord a. However, there have been some proposals to fix this. I assume that if they went through, then it would be possible to define a type which could be interpreted as either a list or a set, with different functor instances in either case.