Janis Voigtlaender wrote:
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 ;-)
Let me be a bit more precise.
A free theorem can be used to prove that any
f :: (a -> b) -> [a] -> [b]
which satisfies
f id = id
also satisfies
f = map (for the Haskell standard map).
Also, a free theorem can be used to prove that any
f :: (a -> b) -> Tree a -> Tree b
for
data Tree a = Node (Tree a) (Tree a) | Leaf a
which satisfies
f id = id
also satsifies
f = fmap
for the following definition:
fmap f (Leaf a) = Leaf (f a)
fmap f (Note t1 t2) = Node (fmap f t1) (fmap f t2)
That gives the desired statement of "unique Functor instances" for the
list type and the above Tree type. And the same kind of proof is
possible for what I called "not-too-exotic" datatypes. And since all
these proofs are essentially the same, it is no doubt possible to give a
generic argument that provides the more general statement that for all
such datatypes exactly one Functor instance exists.
Makes sense?
Ciao, Janis.
--
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:[EMAIL PROTECTED]
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
