Is Haskell's `Const` Functor analogous to the constant functor from category theory?

Question

I understand that many of the names in Haskell are inspired by category theory terminology, and I'm trying to understand exactly where the analogy begins and ends.

The Category Hask

I already know that Hask is not (necessarily) a category due to some technical details about strictness/laziness and seq, but let's put that aside for now. For clarity,

• The objects of Hask are concrete types, that is, types of kind *. This includes function types like Int -> [Char], but not anything that requires a type parameter like Maybe :: * -> *. However, the concrete type Maybe Int :: * belongs to Hask. Type constructors / polymorphic functions are more like natural transformations (or other more general maps from Hask to itself), rather than morphisms.
• The morphisms of Hask are Haskell functions. For two concrete types A and B, the hom-set Hom(A,B) is the set of functions with signature A -> B.
• Function composition is given by f . g. If we are worried about strictness, we might redefine composition to be strict or be careful about defining equivalence classes of functions.

Functors are Endofunctors in Hask

I don't think the technicalities above have anything to do with my confusion below. I think I understand it means to say that every instance of Functor is an endofunctor in the category Hask. Namely, if we have

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

-- Maybe sends type T to (Maybe T) 
data Maybe a = Nothing | Just a

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap _ Nothing  = Nothing

the Functor instance Maybe corresponds to a functor from Hask to Hask in the following way:

• To each concrete type a in Hask, we assign the concrete type Maybe a

• To each morphism f :: A -> B in Hask, we assign the morphism Maybe A -> Maybe B which sends Nothing ↦ Nothing and Just x ↦ Just (f x).

The Constant (endo)Functor

The constant (endo)functor on a category C is a functor Δc : C → C mapping each object of the category C to a fixed object c∈C and each morphism of C to the identity morphism id_c : c → c for the fixed object.

The Const Functor

Consider Data.Functor.Const. For clarity, I will redefine it here, distinguishing between the type constructor Konst :: * -> * -> * and the data constructor Const :: forall a,b. a -> Konst a b.

newtype Konst a b = Const { getConst :: a }

instance Functor (Konst m) where
    fmap :: (a -> b) -> Konst m a -> Konst m b
    fmap _ (Const v) = Const v

This type checks because the data constructor Const is polymorphic:

       v  :: a
(Const v) :: forall b. Konst a b

I can buy that Konst m is an endofunctor in the category Hask, since in the implmenetation of fmap,

• on the left-hand side, Const v manifests itself as a Konst m a, which is ok due to polymorphism
• on the right-hand side, Const v manifests itself as a Konst m b, which is ok due to polymorphism

But my understanding breaks down if we try to think of Konst m :: * -> * as a constant functor in the category-theoretic sense.

• What is the fixed object? The type constructor Konst m takes some concrete type a and gives us a Konst m a, which, at least superficially, is a different concrete type for every a. We really want to map each type a to the fixed type m.

• According to the type signature, fmap takes an f :: a -> b and gives us a Konst m a -> Konst m b. If Konst m were analogous to the constant functor, fmap would need to send every morphism to the identity morphism id :: m -> m on the fixed type m.

Questions

So, here are my questions:

1. In what way is Haskell's Const functor analogous to the constant functor from category theory, if at all?

2. If the two notions are not equivalent, is it even possible to express the category-theoretic constant functor (call it SimpleConst, say) in Haskell code? I gave it a quick try and ran into the same problem with polymorphism wrt phantom types as above:

data SimpleKonst a = SimpleConst Int

instance Functor SimpleConst where
    fmap :: (a -> b) -> SimpleConst a -> SimpleConst b
    fmap _ (SimpleConst x) = (SimpleConst x)

3. If the answer to #2 is yes, If so, in what way are the two Haskell functions related in the category-theoretic sense? That is, SimpleConst is to Const in Haskell as the constant functor is to __?__ in category theory?

4. Do phantom types pose a problem for thinking of Hask like a category? Do we need to modify the definition of Hask so that objects are really equivalence classes of types that would otherwise be identical if not for the presence of a phantom type parameter?

Edit: A Natural Isomorphism?

It looks like the polymorphic function getConst :: forall a,b. Konst a b -> a is a candidate for a natural isomorphism η : (Konst m) ⇒ Δm from the functor Konst m to the constant functor Δm : Hask → Hask, even though I haven't been able to establish yet whether the latter is expressible in Haskell code.

The natural transformation law would be η_x = (Konst m f) . η_y. I'm having trouble proving it, since I'm not sure how to formally reason about the conversion of a (Const v) from type Konst m a to Konst m b, other than handwaving that "a bijection exists!".

Related References

Here is a list of possibly related questions / references not already linked above:

• StackOverflow, "Do all Type Classes in Haskell have a Category-Theoretic Analogue?"
• StackOverflow, "How are functors in Haskell related to functors in category theory?"
• WikiBooks, Haskell/Category Theory

Answer 1

The problem we have here is that a functor is mathematically speaking a dependent pair, but it's a pair where one side (the Type -> Type mapping) lives in Haskell's type-level world, whereas the other side (the (a -> b) -> f a -> f b mapping) lives in the value-level world. Haskell doesn't have a way to express such pairs. The Functor class tricks its way around this limitation by allowing only type constructors as the Type -> Type mapping.
The reason this helps is that type constructors are unique, i.e. every one of them can be assigned a well-defined morphism-mapping through Haskell's typeclass mechanism. But the flip side is that, well, the result is always unique, so you end up with the situation where Konst Int Char and Konst Int Bool are technically speaking different, albeit isomorphic, types.

A more mathematical way of expressing functors would require a separate means of identifying at the type level what functor you mean. Then you only need a type-level mapping (which can be done with type families) and a type→value-level mapping (typeclass):

type family FunctorTyM f a :: Type
class FunctorMphM f where
  fmap' :: (a -> b) -> FunctorTyM f a -> FunctorTyM f b

data KonstFtor a
type instance FunctorTyM (KonstFtor a) b = a
instance FunctorMphM (KonstFtor a) where
  fmap' _ = id

This would still allow you to have also instances for the standard functors:

data IdentityFtor
type instance FunctorTyM IdentityFtor a = a
instance FunctorMphM IdentityFtor where
  fmap' f = f

data ListFtor
type instance FunctorTyM ListFtor a = [a]
instance FunctorMphM ListFtor where
  fmap' f = map f

But it would be more awkward to use in practice. You'll notice that the FunctorMphM class requires -XAllowAmbiguousTypes to compile – that's because f can't be inferred from FunctorTyM f. (We could ameliorate this with injective type families, but that would just get us back to the same issue we started with: the issue is precisely that the const functor is not injective!)

With modern Haskell, that's ok though, it just means you need to be explicit about what functor you're working with. (Arguably, that would often be a good thing anyway!) Full example:

{-# LANGUAGE TypeFamilies, AllowAmbiguousTypes, TypeApplications #-}

type family FunctorTyM f a
class FunctorMphM f where ...

data KonstFtor a
...

data IdentityFtor
...

data ListFtor
...

main :: IO ()
main = do
  print (fmap' @(KonstFtor Int) (+2) 5)
  print (fmap' @IdentityFtor (+2) 5)
  print (fmap' @ListFtor (+2) [7,8,9])

Output:

5
7
[9,10,11]

This approach has some other advantages too. For instance we can finally express that tuples are functors in each of their arguments, not just in the rightmost one:

data TupleFstConst a
type instance FunctorTyM (TupleFstConst a) b = (a,b)
instance FunctorMphM (TupleFstConst a) where
  fmap' f (x,y) = (x, f y)

data TupleSndConst b
type instance FunctorTyM (TupleSndConst b) a = (a,b)
instance FunctorMphM (TupleSndConst b) where
  fmap' f (x,y) = (f x, y)

data TupleFtor
type instance FunctorTyM TupleFtor a = (a,a)
instance FunctorMphM TupleFtor where
  fmap' f (x,y) = (f x, f y)

main :: IO ()
main = do
  print (fmap' @(TupleFstConst Int) (+2) (5,50))
  print (fmap' @(TupleSndConst Int) (+2) (5,50))
  print (fmap' @TupleFtor           (+2) (5,50))

(5,52)
(7,50)
(7,52)

Answer 2

1. Q. In what way is Haskell's Const functor analogous to the constant functor from category theory, if at all?
   A. Const a b sends ant type b to a type isomorphic to a, instead of sending it to a as category-theoretic definition would require. This is not a big deal since isomorphic objects are "really the same object".
2. Q. If the two notions are not equivalent, is it even possible to express the category-theoretic constant functor (call it SimpleConst, say) in Haskell code?
   A. They are not exactly equivalent, but they are equivalent up to an isomorphism, which is good enough. If you want exact equivalence, then it depends on what exactly you mean by "expressing a functor in code". Let's consider the identity functor as it's a bit simpler than Const. You can just write a type alias: type Id a = a and the associated morphism is just id. If you want to write an instance of Functor for this Id, then no, you can't do that in Haskell, because you cannot write class instances for type aliases (perhaps in some other similare language you could do that).
3. Q. [I]n what way are the two Haskell functions related in the category-theoretic sense?
   A. There is no the const functor in category theory. There is a const functor for each object. Haskell Const a is related to such a const functor associated with object a. Haskell Const (no argument) is really a bifunctor (the right projection bifunctor if I'm not mistaken).
4. Q. Do phantom types pose a problem for thinking of Hask like a category? Do we need to modify the definition of Hask so that objects are really equivalence classes of types that would otherwise be identical if not for the presence of a phantom type parameter?
   A. No, it is not a problem. Naturally isomorphic functors (or Functors) are "essentially the same". We say that in category theory "the ConstX functor sends any object to X", but we could just as well choose any functor naturally isomorphic to ConstX and study it instead. It would not change our mathematics in any meaningful way. We choose ConstX simply because it's the easiest one to define. In Haskell, Const X is the easiest one to define, so we use that as our the constant functor.

Addendum.

constIso1 :: Konst x a -> x
constIso1 (Const x) = x
constIso2 :: x -> Konst x a
constIso2 = Const

Answer 3

You're right that Konst m isn't quite a constant functor from a category-theory standpoint. But it's very closely related to one!

type CF m a = m

Now (CF m, id @m) really is a constant functor. I think the main lesson is that while we think of Functor as the class of endofunctors on Hask, it isn't really quite all of them.

I don't believe phantom types per se are an issue. Konst m a and Konst m b are different, but isomorphic, objects.