Example of non-trivial functors

Question

In Haskell, functors can almost always be derived, is there any case where a type is a functor and satisfies functor laws (such as fmap id == id) but cannot be derived according to a simple set of rules?

And what about Foldable, Traversable, Semigroup and others? Is there any non-trivial cases available?

Answer 1

Here's kind of a fun argument I just stumbled on. (It's late so I wonder if it will be sensical tomorrow)

We can construct the type of proofs of SK reducibility as a GADT:

infixl 9 :%:
data Term = S | K | Term :%: Term

-- small step, you can get from t to t' in one step
data Red1 t t' where
    Red1S :: Red1 (S :%: x :%: y :%: z) (x :%: z :%: (y :%: z))
    ...

Now let's make a type which hides its functorhood at the end of a reduction chain.

data Red t a where
    RedStep :: Red1 t t' -> Red t' a -> Red t a
    RedK    :: a                     -> Red K a
    RedS    :: (a -> Bool)           -> Red S a

Now Red t is a Functor if t normalizes to K, but not if it normalizes to S -- an undecidable problem. So perhaps you can still follow a "simple set of rules", but if you allow GADTs, the rules have to be powerful enough to compute anything.

(There is an alternative formulation which I find rather elegant, but maybe less demonstrative: if you drop the RedK constructor, then Red t is a Functor if and only if the type system can express that the reduction of t diverges -- and sometimes it diverges but you can't prove it, and my mind boggles about whether it's really a functor in that case or not)

Answer 2

Explicitly empty parametric types can be made into functors automatically:

data T a deriving Functor

However, implicitly empty ones can not:

import Data.Void
data T a = K a (a -> Void)
    deriving Functor  -- fails
{-
error:
    • Can't make a derived instance of ‘Functor T’:
        Constructor ‘K’ must not use the type variable in a function argument
    • In the data declaration for ‘T’
-}

However,

instance Functor T where
   fmap f (K x y) = absurd (y x)

is arguably a legal instance.

One could argue that, exploiting bottoms, one can find a counterexample to the functor laws for the instance above. In such case, however, I wonder if all the "standard" functor instances are actually lawful, even in the presence of bottoms. (Maybe they are?)

Answer 3

There are no non-trivial functors in the sense of the question. All functors can be derived mechanically as sums (Either) and products (Tuple) of the Identity and the Const functor. See the section about Functorial Algebraic Data Types for how this construction works in detail.

On a higher level of abstraction this works because Haskell's type form a Cartesian Closed Category where terminal objects, all products and all exponentials exist.