What is the significance of the id member's type in the Category class?

Question

In PureScript, the Category class is defined in Control.Category as follows:

class Semigroupoid a <= Category a where
    id :: forall t. a t t

What does the type a t t signify and what is the rationale behind defining id this way?

Answer 1

We could have defined function composition and the identity function like in Haskell:

id :: a -> a
(.) :: (b -> c) -> (a -> b) -> a -> c

This is fine. However, there are other things which look and act like functions, for which we'd like to define composition and identities. They obey the same laws, so it makes sense to reuse the symbols, and define them in a common type class.

Why is this a useful generalization? One example is the Kleisli arrow for a monad. These are functions of the form a -> m b for some monad. It's very useful to be able to compose these things like functions, and it's sometimes useful to talk about composition in generality, whether it is for functions, or Kleisli arrows, or some other function-like thing.

The Category class becomes more useful when paired with the Strong class from the purescript-profunctor library. This is because a strong profunctor which is also a category is equivalent to an Arrow. There is plenty of existing literature documenting the usefulness of the Arrow class.

To answer your original question, notice that the types above are a special case of the more general types defined in the Semigroupoid and Category classes:

id :: k a a
compose :: k b c -> k a b -> k a c

since we can just pick k to be the function arrow (->).