Can smart-constructor types have multiple valid Functor instances?

Question

These two rules about Functors are fairly well-known:

1. You can't make a Functor if the type parameter appears contravariantly
2. Any type has at most one valid Functor instance

But if you cheat slightly, you can break the first rule. Take the Hughes list, for example:

data HList a = UnsafeHList ([a] -> [a])

pattern HList a <- UnsafeHList (($ []) -> a)
    where HList a = UnsafeHList (a ++)

instance Functor HList where
    fmap f (HList a) = HList (map f a)

-- instances necessary to make HList useful, but irrelevant to this example, have been omitted

As long as you make the assumption that all HLists will be made through the smart constructor, that Functor instance is lawful, even though a appears contravariantly.

My question: can you use a similar technique to break the second rule? Are there any types that have two different valid Functor instances if you assume that they'll always be made through smart constructors?

Royroyal

(ehem) Very incidentally, you can make a difference list functorial without cheating by using Yoneda: newtype HList a = HList (forall b. (a -> b) -> [b] -> [b]) – Pelag

@Pelag That one does seem to work and have good asymptotics. I wonder why it's not more popular compared to the smart-constructor approach. – Royroyal

(co)yoneda is a great trick for functorizing things, under appreciated. Maybe because it has a scary name (never stopped us before...) – Pelag

Answer 1

Absolutely. Suppose you have

newtype Foo a = Foo Bool

mkFoo = Foo True

Here are its two Functor instances:

instance Functor Foo where
  fmap _ (Foo x) = Foo x

instance Functor Foo where
  fmap _ !_ = mkFoo

Swacked

Yep, this looks legit after all, though it still feels unsatisfying for some reason. – Royroyal

@JosephSible-ReinstateMonica, is the edited version more satisfying? – Swacked

How is that “smart” instance not equivalent to the “obvious” one? Is it about the strictness? Then you could do the same for any functor. – Bohs

@Bohs Consider fmap id (Foo False). If not for the smart-constructor restriction, that would be a witness of breaking the identity law. – Royroyal

"at most one valid Functor instance" assumes lawful instances though, that's probably why it feels unsatisfactory. – Hynes

The "smart-constructor" restriction prevents you from observng the boolean, which makes that instance observationally equivalent to the obvious one. Basically, they're still kinda the same. – Hynes

I'm not sure if this is quite right. I'd argue that a type isn't actually just a type, but also the equivalence we choose to use on that type. Foo can be "completed" with two equivalences: it can have two distinct values or just one. In the first case, the "const" instance is invalid. In the second case, the "identity" and "const" instances are both valid, but... they're also equal. Is there a type (defined by both the actual Haskell type and the equivalence we want to use on it) that actually has two valid, inequivalent (by that equivalence) Functor instances? – Duleba

@HTNW, I doubt it very much, but I'm not sure how to prove that. An invalid Functor instance must, by parametricity, violate the identity law. Considering the values of the type as representatives can fix that. So we'd need that fix to still violate the composition law. I think that means your abstraction can't be mapped faithfully to any Haskell type, which seems fairly implausible. – Swacked

@leftaroundabout, that bang pattern isn't very interesting, but it's necessary to deal with the fact that mkFoo is never the only way to make a Foo—undefined is always an option, and we want fmap id undefined = undefined. – Swacked

After reading the other comments, I realize why I still feel like this is unsatisfying now: the assumption that you have to make for the instance to be valid also prevents you from observing the difference between that instance and the normal one. – Royroyal

@JosephSible-ReinstateMonica, yeah, that's a point. I suspect there's no other way, but I will think on it. – Swacked