I'm trying to build a custom category:

type Cat i = i -> i -> Type

class Category (h :: Cat i) where
  id :: h a a
  (.) :: h b c -> h a b -> h a c

-------------------------------------------------

data HFun (l :: [Type]) (l' :: [Type]) where
    HFunNil :: HFun '[] '[]
    (:->:) :: (a -> b) -> HFun as bs -> HFun (a ': as) (b ': bs)

class Id x where
    id :: x

instance Id (HFun '[] '[]) where
    id = HFunNil

instance Id (HFun l l) => Id (HFun (a ': l) (a ': l)) where
    id = Pr.id :->: id  

instance Category HFun where
  id = id

but this fails to compile with: No instance for (Id (HFun a a)) arising from a use of ‘id’ :( any help/suggestion is much appreciated

CodePudding user response：

You need to add a dummy HFunId :: HFun as as constructor to your type, or add constraints to your category

type Cat :: Type -> Type
type Cat ob = ob -> ob -> Type

type     Empty :: ob -> Constraint
class    Empty a
instance Empty a

type  Category :: Cat ob -> Constraint
class Category (cat :: Cat ob) where
  type Obj (cat :: Cat ob) :: ob -> Constraint
  type Obj _ = Empty

  id  :: Obj cat a => cat a a
  (.) :: cat b c -> cat a b -> cat a c

Then you can define a constraint that allows you to pattern match on the spine of a list:

type Spine :: [k] -> Type
data Spine as where
  Spineless :: Spine '[]
  Spine     :: Spine as -> Spine (a:as)

type  SpineI :: [k] -> Constraint
class SpineI as where
  spine :: Spine as

instance SpineI '[] where
  spine :: Spine '[]
  spine = Spineless

instance SpineI as => SpineI (a:as) where
  spine :: Spine (a:as)
  spine = Spine spine

Then you can define id for HFun :: Cat [Type]:

instance Category HFun where
  type Obj HFun = SpineI

  id :: SpineI as => HFun as as
  id = go spine where

    go :: forall xs. Spine xs -> HFun xs xs
    go Spineless  = HFunNil
    go (Spine as) = id :->: go as

  (.) :: HFun bs cs -> HFun as bs -> HFun as cs
  (.) = undefined