Reputation: 1509
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.
Upvotes: 2
Views: 336
Reputation: 120711
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 unsafeCoerce
s 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.
Upvotes: 3