Luke Palmer lrpalmer at gmail.com writes:
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
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
Janis Voigtlaender voigt at tcs.inf.tu-dresden.de writes:
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
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
