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?
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 (->)
.