Haskell 的“Const”函子是否类似于范畴论中的常数函子？

Question

我知道 Haskell 中的许多名称都受到范畴论术语的启发，我正试图准确理解类比的开始和结束位置。

分类Hask

我已经知道 Hask is not (necessarily) a category 是因为一些关于严格/懒惰和 seq 的技术细节，但现在让我们把它放在一边。为了清楚起见，

• Hask 的对象是具体类型，即类型为*。这包括像Int -> [Char] 这样的函数类型，但不包括像Maybe :: * -> * 这样需要类型参数的任何东西。但是，具体类型Maybe Int :: * 属于Hask。类型构造函数/多态函数更像是自然变换（或从Hask 到自身的其他更一般的映射），而不是态射。
• Hask 的态射是 Haskell 函数。对于A 和B 这两种具体类型，hom 集Hom(A,B) 是签名为A -> B 的函数集。
• 函数组合由f . g 给出。如果我们担心严格性，我们可能会 redefine composition 严格或小心 defining equivalence classes 的函数。

Functors 是 Hask 中的 Endofunctors

我认为上面的技术细节与我在下面的困惑没有任何关系。我想我理解这意味着说every instance of Functor is an endofunctor in the category Hask。也就是说，如果我们有

class Functor (F :: * -> *) where
    fmap :: (a -> b) -> F a -> F b

-- Maybe sends type T to (Maybe T) 
data Maybe a = Nothing | Just a

instance Functor Maybe where
  fmap f (Just x) = Just (f x)
  fmap _ Nothing  = Nothing

Functor 实例Maybe 对应于从Hask 到Hask 的函子，方式如下：

• 对于Hask中的每个具体类型a，我们分配具体类型Maybe a

• 对于Hask 中的每个态射f :: A -> B，我们分配发送Nothing ↦ Nothing 和Just x ↦ Just (f x) 的态射Maybe A -> Maybe B。

常数（endo）函子

类别 C 上的 constant (endo)functor 是一个函子 Δc : C → C，将类别 C 的每个对象映射到固定对象 c∈C，并将 C 的每个态射映射到固定对象的恒等态射 id_c : c → c。

ConstFunctor

考虑Data.Functor.Const。为了清楚起见，我在这里重新定义，区分类型构造函数Konst :: * -> * -> *和数据构造函数Const :: forall a,b. a -> Konst a b。

newtype Konst a b = Const { getConst :: a }

instance Functor (Konst m) where
    fmap :: (a -> b) -> Konst m a -> Konst m b
    fmap _ (Const v) = Const v

这个类型检查是因为数据构造函数Const是多态的：

       v  :: a
(Const v) :: forall b. Konst a b

我可以认为Konst m 是Hask 类别中的内函子，因为在fmap 的实现中，

• 在左侧，Const v 显示为 Konst m a，由于多态性，这没关系
• 在右侧，Const v 显示为 Konst m b，由于多态性，这是可以的

但如果我们试图将 Konst m :: * -> * 视为范畴论意义上的常数函子，我的理解就会崩溃。

• 什么是固定对象？类型构造函数Konst m 接受一些具体类型a 并为我们提供Konst m a，至少从表面上看，它是每个a 的不同具体类型。我们真的很想将每个类型 a 映射到固定类型 m。

• 根据类型签名，fmap 接受一个f :: a -> b 并给我们一个Konst m a -> Konst m b。如果Konst m 类似于常量函子，则fmap 需要将每个态射发送到固定类型m 上的恒等态射id :: m -> m。

问题

所以，这是我的问题：

1. Haskell 的 Const 函子在哪些方面类似于范畴论中的常数函子（如果有的话）？

2. 如果这两个概念不等价，是否甚至可以在 Haskell 代码中表达范畴论常数函子（比如说，称之为SimpleConst）？我快速尝试了一下，遇到了与上述幻象类型的多态性相同的问题：

data SimpleKonst a = SimpleConst Int

instance Functor SimpleConst where
    fmap :: (a -> b) -> SimpleConst a -> SimpleConst b
    fmap _ (SimpleConst x) = (SimpleConst x)

1. 如果#2 的答案是肯定的，如果是，那么在范畴论意义上，这两个 Haskell 函数有什么关系？也就是说，SimpleConst 对应于 Haskell 中的 Const，就像常量函子对应于范畴论中的 __?__？

2. 幻象类型是否会给将Hask 视为一个类别造成问题？我们是否需要修改Hask 的定义，使对象真正成为类型的等价类，如果没有幻像类型参数，这些类型本来是相同的？

编辑：自然同构？

看起来多态函数getConst :: forall a,b. Konst a b -> a是从函子Konst m到常数函子Δm : Hask → Hask的自然同构η : (Konst m) ⇒ Δm的候选者，尽管我还不能确定后者是否可以用 Haskell 代码表达。

自然变换法则是η_x = (Konst m f) . η_y。我无法证明这一点，因为我不知道如何正式推理 (Const v) 从类型 Konst m a 到 Konst m b 的转换，除了挥手说“存在双射！”。

相关参考资料

以下是上面尚未链接的可能相关问题/参考的列表：

• 堆栈溢出，"Do all Type Classes in Haskell have a Category-Theoretic Analogue?"
• 堆栈溢出，"How are functors in Haskell related to functors in category theory?"
• 维基百科，Haskell/Category Theory

Answer 1

我们这里遇到的问题是，从数学上讲，函子是一个依赖对，但它的一侧（Type -> Type 映射）存在于 Haskell 的类型级世界中，而另一侧（(a -> b) -> f a -> f b映射）生活在价值层面的世界中。 Haskell 没有办法表达这样的对。 Functor 类通过只允许 类型构造函数 作为 Type -> Type 映射来绕过这个限制。
这有帮助的原因是类型构造函数是唯一的，即它们中的每一个都可以通过 Haskell 的类型类机制分配一个定义良好的态射映射。但另一方面是，结果总是唯一的，所以你最终会遇到Konst Int Char 和 Konst Int Bool 在技术上讲不同的情况，尽管是同构的类型。

表达函子的更数学的方式需要一种单独的方法来在类型级别识别您的意思函子。那么你只需要一个类型级映射（可以用类型族来完成）和一个类型→值级映射（typeclass）：

type family FunctorTyM f a :: Type
class FunctorMphM f where
  fmap' :: (a -> b) -> FunctorTyM f a -> FunctorTyM f b

data KonstFtor a
type instance FunctorTyM (KonstFtor a) b = a
instance FunctorMphM (KonstFtor a) where
  fmap' _ = id

这仍然允许您拥有标准仿函数的实例：

data IdentityFtor
type instance FunctorTyM IdentityFtor a = a
instance FunctorMphM IdentityFtor where
  fmap' f = f

data ListFtor
type instance FunctorTyM ListFtor a = [a]
instance FunctorMphM ListFtor where
  fmap' f = map f

但实际使用起来会比较尴尬。你会注意到FunctorMphM 类需要-XAllowAmbiguousTypes 才能编译——这是因为f 不能从FunctorTyM f 推断出来。 （我们可以使用单射类型族来改善这一点，但这只会让我们回到我们开始讨论的同一个问题：问题恰恰是 const 函子 不是 单射的！）

使用现代 Haskell，ok 不过，这只是意味着您需要明确说明您正在使用的函子。 （可以说，这通常是一件好事！）完整示例：

{-# LANGUAGE TypeFamilies, AllowAmbiguousTypes, TypeApplications #-}

type family FunctorTyM f a
class FunctorMphM f where ...

data KonstFtor a
...

data IdentityFtor
...

data ListFtor
...

main :: IO ()
main = do
  print (fmap' @(KonstFtor Int) (+2) 5)
  print (fmap' @IdentityFtor (+2) 5)
  print (fmap' @ListFtor (+2) [7,8,9])

输出：

5
7
[9,10,11]

这种方法还有其他一些优点。例如，我们最终可以在其参数的每个中表示元组是函子，而不仅仅是在最右边的一个：

data TupleFstConst a
type instance FunctorTyM (TupleFstConst a) b = (a,b)
instance FunctorMphM (TupleFstConst a) where
  fmap' f (x,y) = (x, f y)

data TupleSndConst b
type instance FunctorTyM (TupleSndConst b) a = (a,b)
instance FunctorMphM (TupleSndConst b) where
  fmap' f (x,y) = (f x, y)

data TupleFtor
type instance FunctorTyM TupleFtor a = (a,a)
instance FunctorMphM TupleFtor where
  fmap' f (x,y) = (f x, f y)

main :: IO ()
main = do
  print (fmap' @(TupleFstConst Int) (+2) (5,50))
  print (fmap' @(TupleSndConst Int) (+2) (5,50))
  print (fmap' @TupleFtor           (+2) (5,50))

(5,52)
(7,50)
(7,52)

Answer 2

1. 问。 Haskell 的 Const 仿函数在哪些方面类似于范畴论中的常量仿函数？
   A. Const a b 将 ant 类型 b 发送到与 a 同构的类型，而不是根据类别理论定义将其发送到 a。这没什么大不了的，因为同构对象“实际上是同一个对象”。
2. 问。如果这两个概念不等价，是否甚至可以在 Haskell 代码中表达范畴论常数函子（称之为SimpleConst）？
   A. 它们不完全等价，但它们等价于同构，这已经足够好了。如果您想要精确等价，那么这取决于您“在代码中表达函子”的确切含义。让我们考虑恒等函子，因为它比 Const 更简单一些。你可以只写一个类型别名：type Id a = a，相关的态射就是id。如果您想为此 Id 编写 Functor 的实例，那么不，您不能在 Haskell 中这样做，因为您不能为类型别名编写类实例（也许在其他类似的语言中您可以这样做） .
3. 问。 [I]在范畴论意义上，这两个 Haskell 函数有什么关系？
   A. 范畴论中没有 the const 函子。每个对象都有 a const 仿函数。 Haskell Const a 与对象 a 关联的此类 a const 函子有关。 Haskell Const（无参数）实际上是一个双函子（如果我没记错的话，就是正确的投影双函子）。
4. 问。幻象类型是否会在将 Hask 视为一个类别时造成问题？我们是否需要修改 Hask 的定义，使对象真正成为类型的等价类，如果不存在幻像类型参数，这些类型本来是相同的？
   A. 不，这不是问题。自然同构函子（或Functors）“本质上是相同的”。我们说在范畴论中“ConstX 函子将任何对象发送给 X”，但我们也可以选择任何自然同构于 ConstX 的函子来研究它。它不会以任何有意义的方式改变我们的数学。我们选择 ConstX 仅仅是因为它是最容易定义的。在 Haskell 中，Const X 是最容易定义的，所以我们使用它作为我们的 the 常量仿函数。

附录。

constIso1 :: Konst x a -> x
constIso1 (Const x) = x
constIso2 :: x -> Konst x a
constIso2 = Const

Answer 3

你说得对，从范畴论的角度来看，Konst m 相当不是一个常数函子。但它与一个密切相关！

type CF m a = m

现在(CF m, id @m) 确实是一个常量函子。我认为主要的教训是，虽然我们将Functor 视为Hask 上的内函子类，但实际上并不是全部。

我不认为幻像类型本身是一个问题。 Konst m a 和 Konst m b 是不同但同构的对象。