haskell - 我们如何在 Haskell 中构建明确的类别？

Question

与范畴的数学思想相对应，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

当前错误是无法将预期类型“TcArrowType a a”与实际类型“TcObjectType -> TcArrowType TcObjectType TcObjectType”匹配。 TcArrow TcObject TcObject 应该是代表唯一箭头的值，但由于某种原因，编译器似乎将其视为函数。

有合理的方法吗？

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

Answer 1

tl;dr 请参阅 https://gist.github.com/leftaroundabout/d5347d06dfcfc1d8ce796bb2966b3343以获得完整的、可编译的、安全的版本。

---

问题是需要 Control.Category.id 来量化给定种类的所有类型:

class Category c where
  id :: <b>∀ a</b> . 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 类是多种类(这在文档中并不明显)，因此您可以使用而不是您的数据 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::TcObjectKind 推断出 o ~ TcObject。但你可以手动告诉它:

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 。在我看来，这不是 unsafeCoerce 的错，而是 GHC 的错，但这仍然不是一个很好的解决方案。

---

^†_{迂腐地说，它不是一个类型，而是一个类型级别的值。}

---

对于比终端类别具有更多对象和箭头的更复杂的工作和类别，您需要使其更加规范，而不是在 id 中手动 unsafeCoerce。这本质上就是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

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