[Haskell-cafe] Unique functor instance
voigt at tcs.inf.tu-dresden.de
Tue Nov 25 08:36:16 EST 2008
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]
f id = id
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
data Tree a = Node (Tree a) (Tree a) | Leaf a
f id = id
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.
Dr. Janis Voigtlaender
mailto:voigt at tcs.inf.tu-dresden.de
More information about the Haskell-Cafe