Haskell - 尽管定义了所有实例，但没有 (Id (HFun a a)) 的实例答案

【问题标题】：Haskell - No instance for (Id (HFun a a)) although all instances are definedHaskell - 尽管定义了所有实例，但没有 (Id (HFun a a)) 的实例
【发布时间】：2022-07-28 02:51:07
【问题描述】：

我正在尝试构建一个自定义类别：

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

但这无法编译：没有因使用“id”而产生的 (Id (HFun a a)) 实例 :(非常感谢任何帮助/建议

【问题讨论】：

您报道了a=[] 和a=(b:l) 的案例。这直观地涵盖了所有情况，但 GHC 不会接受，而是需要一个实例 Id (HFun a a)（或更通用的实例，Id (HFun a1 a2)）。我不确定如何解决这个问题。
您能否提供一个完整的示例供我们测试？

标签： haskell

【解决方案1】：

您需要为您的类型添加一个虚拟的HFunId :: HFun as as 构造函数，或者为您的类别添加约束

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

然后您可以定义一个约束，允许您在列表的主干上进行模式匹配：

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

那么你可以为HFun :: Cat [Type]定义id：

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) = Prelude.id :->: go as

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

【讨论】：