4
$\begingroup$

So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors.

But it this always the case? What's throwing me off is Haskell's Functor typeclass:

class Functor f :: * -> * where
   fmap :: (a -> b) -> (f a -> f b)

If all type constructors were a priori functors, there would be no need to define a special type-class. But I can't think of any type-constructors that fail to satisfy the Functor type-class: product, sum, function, list, set, option, etc.

I also cannot imagine the utility of a type-constructors that is "one-half" of a functor, i.e. it has a map from objects to objects, but no map between morphisms.

$\endgroup$
8
$\begingroup$

One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to Ord), or even replace the values with a type which is not an instance of Ord at all.

A possibly less-obvious example is a contravariant endofunctor. Consider:

data Tricky a = Tricky (a -> String)

Try writing a Functor instance for this.

But that doesn't mean you can't construct a functor-like class which it the type does satisfy. This Tricky type, after all, is a contravariant functor:

-- Somebody has probably already implemented this in a library
-- somewhere, with a better name.
class ContraFunctor f :: * -> * where
    contramap :: (b -> a) -> (f a -> f b)

instance ContraFunctor Tricky where
    contramap f (Tricky t) = Tricky (t . f)

and like fmap, it must satisfy some axioms which are left as an exercise.

What's interesting, though, is that you can usually come up with a functor-like class (and its axioms, of course) which applies type substitutions in a principled way, from the types of the functions which comprise their API.

The full details are beyond the scope, but it's based on a remarkable property of a polymorphic function is known as the "free theorem". Any polymorphic function has a theorem that it satisfies simply by virtue of being polymorphic, and the theorem is mechanically derivable from its type.

What the theorem essentially states is that a polymorphic function commutes with a type substitution. This is what "polymorphic" really means.

Let's take reverse as an example:

reverse :: forall a. [a] -> [a]

There are no constraints whatsoever on the type of a, so it will commute with any type substition:

forall f :: A -> B. fmap f . reverse = reverse . fmap f

(Remember, . is function composition in Haskell.)

This is true for any types A and B. In a deep sense, this is what the "forall" actually means in the type of reverse.

Now consider sort:

sort :: forall a. Ord a => [a] -> [a]

The problem here is that Ord is a constraint on the type of a. What this means is that this is a constraint on any type substitution: it must be a homomorphism of Ord.

forall f :: A -> B.
    (forall x y : A, compare x y = compare (f x) (f y))
    => fmap f . sort = sort . fmap f

That extra precondition, that f is an Ord-homomorphism, intuitively means that f is a function which preserves the order. This should make sense: if a type substitution doesn't change the ordering of elements, then that type substitution commutes with sort.

But here's my favourite example of all. Suppose that F and G are functors. Now consider this function:

eta :: forall a. F a -> G a

The free theorem of this function is:

forall f : A -> B.  fmap f . eta = eta . fmap f

Note that the two fmaps are different instances; the first one is the instance for G and the second is the instance for F. What this is saying is that eta, by virtue of its type alone, is a natural transformation.

$\endgroup$
  • $\begingroup$ Thanks for you detailed response! 1. For the binary search tree constructor BST a, I don't think this is a counter-example, because it's not actually a type-constructor. A type-constructor has to be defined on every type; limiting the domain to ordered types precludes this. 2. A contravariant functor is just a normal covariant functor in the dual category, so while technically this is a counter-example, it's not a very interesting one. 3. You're talking about natural transformations. This fact very recently blew my mind. 4. I am going to read the paper you linked $\endgroup$ – gardenhead Oct 13 '16 at 23:41
  • $\begingroup$ In Haskell, BST could be a generalised algebraic datatype. GADTs allow type constructors to be qualified with constraints such as Ord. See wiki.haskell.org/Data_declaration_with_constraint $\endgroup$ – Pseudonym Oct 14 '16 at 1:58
  • $\begingroup$ How do GADTs fit into category theory, if at all? $\endgroup$ – gardenhead Oct 14 '16 at 1:59
  • $\begingroup$ Well enough. They have an obvious Church encoding representation, so in that sense they don't really introduce anything new. $\endgroup$ – Pseudonym Oct 14 '16 at 2:00
  • 1
    $\begingroup$ Implicit type parameters always bothered me in Haskell and SML. Having to explicitly instantiate the polymorphic function with a specific type makes it much clearer what's going on. However, I think we can assume that is being done "under the hood" with type inference. With regards to your second comment, to me the intuition goes the other way; understanding what a natural transformation was made me "get" polymorphic functions. I mean, I understood them before, but category theory showed them in a new light. $\endgroup$ – gardenhead Oct 14 '16 at 2:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.