How can we build explicit categories in Haskell?

Corresponding with the mathematical idea of a category, Haskell has a Category typeclass. I'd like to build some small finite categories and work with them, along the lines of the book Computational Category Theory but with better type-checking.

For example, in math there is a small but important category called the "terminal category", which has exactly one object, and one arrow which is that object's identity. Here's my best attempt:

data TcObjectType = TcObject
data TcArrowType a0 a1 where
  TcArrow :: TcObjectType -> TcObjectType -> TcArrowType TcObjectType TcObjectType
instance Category TcArrowType where
  id TcObject = TcArrow TcObject TcObject
  (TcArrow TcObject TcObject) . (TcArrow TcObject TcObject) = TcArrow TcObject TcObject

The current error is Couldn't match expected type ‘TcArrowType a a’ with actual type ‘TcObjectType -> TcArrowType TcObjectType TcObjectType’. TcArrow TcObject TcObject is supposed to be the value representing the unique arrow, but for some reason, the compiler seems to be treating it as a function.

Is there a reasonable way to do this?

Edit: I want to describe any finite category, not just the terminal category. This means I want to say explicitly that arrow X goes from object A to object B. Probably the next example would be the category with two objects and two parallel arrows between them.

Solution

tl;dr See https://gist.github.com/leftaroundabout/d5347d06dfcfc1d8ce796bb2966b3343 for a full, compiling, safe version.

The problem is the Control.Category.id is required to quantify over all types of the given kind:

class Category c where
  id :: ∀ a . c a a
  ...

IOW, if the object are of kind Type (as your TcObject is), then a Category instance must have all Haskell types as objects, which of course immediately disqualifies the terminal category as an instance.

There are several different alternative category classes around that allows specifying a constraint on the choice of objects; with constrained-categories the instance would look thus:

{-# LANGUAGE TypeFamilies, ConstraintKinds    #-}

import qualified Control.Category.Constrained.Class as CC

instance CC.Category TcArrowType where
  type Object TcArrowType a = a ~ TcObjectType
  id = TcArrow TcObject TcObject
  TcArrow TcObject TcObject . TcArrow TcObject TcObject = TcArrow TcObject TcObject

But there's an arguably more elegant alternative: since your object isn't really used as a type at all (you use it as a type to tag the arrows with runtime values, but that information is redundant), there's no point having it be of kind Type in the first place. Indeed the standard Category class is poly-kinded (which is not really evident from the documentation), and therefore you can use instead of your data TcObjectType = TcObject a lifted data constructor to express the same thing:

{-# LANGUAGE DataKinds, KindSignatures #-}

data TcObjectKind = TcObject
data TcArrowType (a₀ :: TcObjectKind) (a₁ :: TcObjectKind) where
  TcArrow :: TcArrowType 'TcObject 'TcObject
instance Category TcArrowType where
  id = TcArrow
  TcArrow . TcArrow = TcArrow

...or at least that's how it would conceptually look. Actually this doesn't quite work, because although TcObject is the only type^† of kind TcObjectKind, the compiler does not automatically infer that o ~ TcObject for every o :: TcObjectKind. But you can manually tell it:

import Unsafe.Coerce

instance Category TcArrowType where
  id = unsafeCoerce TcArrow    -- Safe because `a` can only ever be `TcObject`.

@dfeuer remarks that this is actually not quite safe because of a quirk in how GHC handles type families vs type constructors, see https://gist.github.com/treeowl/6104ef553dadf0d1faf01da0850ddb01. IMO this is not unsafeCoerces fault but GHC's, but still this isn't exactly a nice solution.

^†_{To be pedantic it's not a type, but a type-level value.}

For more sophisticated work and categories with more objects&arrows than the terminal category, you'll want to make this a bit more disciplined instead of manual unsafeCoerce in id. This is essentially the problem that singletons are supposed to solve.

{-# LANGUAGE TemplateHaskell, QuasiQuotes     #-}
{-# LANGUAGE DataKinds, KindSignatures        #-}
{-# LANGUAGE TypeFamilies, GADTs              #-}

import Data.Singletons.TH

$(singletons [d|
   data TcObjectKind = TcObject
  |])

data TcArrowType (a₀ :: TcObjectKind) (a₁ :: TcObjectKind) where
  TcArrow :: TcArrowType 'TcObject 'TcObject

tcId :: ∀ a . SingI a => TcArrowType a a
tcId = case sing :: Sing a of
  STcObject -> TcArrow

This now generalises to categories with multiple objects, like

$(singletons [d|
   data Trap = Free | Trapped
  |])

data TrapArrowType (a₀ :: Trap) (a₁ :: Trap) where
  StillFree :: TrapArrowType 'Free 'Free
  Falling :: TrapArrowType 'Free 'Trapped
  Stuck :: TrapArrowType 'Trapped 'Trapped

trapId :: ∀ a . SingI a => TrapArrowType a a
trapId = case sing :: Sing a of
  SFree -> StillFree
  STrapped -> Stuck

Unfortunately, with singletons we're back at the problem that we have a SingI a constraint that the base Category class cannot provide. But again, the constrained-categories version can.