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

18

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

haskell functor category-theory phantom-types

Share

Improve this question

edited Apr 21 at 6:20

Benjamin Bray

asked Apr 21 at 5:43

Benjamin BrayBenjamin Bray

34422 silver badges99 bronze badges

1

• 3
  Forget Const. The Haskell identity functor isn't the categorical identity either. It doesn't matter because Id a and a are isomorphic, with an obvious bijection. Now can you find one between Konst a x and a? – n. 'pronouns' m. Apr 21 at 6:34

Add a comment  |