我们如何在Haskell中建立显式类别？

如何解决我们如何在Haskell中建立显式类别？

与类别的数学概念相对应，Haskell具有Category typeclass。我想建立一些小的有限类别并按照the book Computational Category Theory的方式与它们一起使用，但要有更好的类型检查。

例如，在数学中，有一个很小但很重要的类别，称为“终端类别”，它只有一个对象，而一个箭头是该对象的标识。这是我的最佳尝试：

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

当前错误为Couldn't match expected type ‘TcArrowType a a’ with actual type ‘TcObjectType -> TcArrowType TcObjectType TcObjectType’。 TcArrow TcObject TcObject应该是代表唯一箭头的值，但是由于某些原因，编译器似乎将其视为函数。

有合理的方法吗？

编辑：我想描述任何有限类别，而不仅仅是终端类别。这意味着我想明确地说箭头X从对象A到对象B。下一个示例可能是类别，其中包含两个对象以及它们之间的两个平行箭头。

解决方法

tl; dr 有关完整的，编译的安全版本，请参见https://gist.github.com/leftaroundabout/d5347d06dfcfc1d8ce796bb2966b3343。

问题在于，Control.Category.id必须量化给定类型的所有类型的：

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

IOW，如果对象属于Type类型（如您的TcObject一样），则Category实例必须具有 all 个Haskell类型作为对象，哪个当然会立即取消终端类别的资格。

周围有几种不同的替代类别类，它们允许在选择对象时指定约束。使用constrained-categories时，实例将如下所示：

{-# 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

但是有一个更优雅的选择：由于您的对象实际上并没有真正用作类型（您可以将它用作用于标记运行时值的箭头的类型，但是该信息是多余的），因此没有意义首先是Type类型。确实，标准Category类是 polykinded （从文档中不能真正看出来），因此您可以使用提升的数据代替data TcObjectType = TcObject构造器表示同一件事：

{-# 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

...或者至少在概念上是这样。实际上，这不是有效，因为尽管TcObject 是唯一的类型TcObjectKind的类型^†，编译器不会自动为每个o ~ TcObject推断那个o :: TcObjectKind。但是您可以手动告诉它：

import Unsafe.Coerce

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

@dfeuer指出，由于GHC处理类型族与类型构造器的方式存在古怪之处，因此这实际上并不完全安全，请参阅https://gist.github.com/treeowl/6104ef553dadf0d1faf01da0850ddb01。 IMO，这不是unsafeCoerce的错，而是GHC的错，但这仍然不是一个很好的解决方案。

^†_{要学究的不是类型，而是类型级别的值。}

对于比终端类别更复杂的工作和具有更多对象和箭头的类别，您需要使其更加严格，而不是unsafeCoerce中的手册id。本质上，这是singletons应该解决的问题。

{-# 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

这现在可以概括为具有多个对象的类别，例如

$(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

不幸的是，对于单例，我们回到了一个问题，即我们有一个SingI a约束，基类Category无法提供该约束。但是，constrained-categories版本也可以。