[Haskell-cafe] Unique functor instance

[Janis Voigtlaender]

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:voigt at tcs.inf.tu-dresden.de