Haskell 的 `Const` 函子是否类似于范畴论中的常数函子？ 类别HaskFunctor 是 Hask常量endo函子id_c : c → c Const问题编辑：自然同构？相关参考资料

如何解决Haskell 的 `Const` 函子是否类似于范畴论中的常数函子？ 类别HaskFunctor 是 Hask常量endo函子id_c : c → c Const问题编辑：自然同构？相关参考资料

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

类别Hask

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

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

Functor 是 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 的函子，如下所示：

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

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

常量（endo）函子

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

id_c : c → c Const

考虑Data.Functor.Const。为了清楚起见，我将在这里重新定义它，区分类型构造函数 Functor 和数据构造函数 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 上的恒等态射 id :: m -> m。

问题

那么，这是我的问题：

1. Haskell 的 m 函子与范畴论中的常数函子有何相似之处？

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

SimpleConst

3. 如果#2 的答案是肯定的，如果是，那么在范畴论意义上，这两个 Haskell 函数以何种方式相关？也就是说，data SimpleKonst a = SimpleConst Int instance Functor SimpleConst where fmap :: (a -> b) -> SimpleConst a -> SimpleConst b fmap _ (SimpleConst x) = (SimpleConst x) 在 Haskell 中与 SimpleConst 的关系就像常数函子在范畴论中与 Const 的关系一样？

4. 幻像类型是否会导致将 __?__ 视为类别的问题？我们是否需要修改 Hask 的定义，以便对象真的是类型的等价类，如果没有幻像类型参数的存在，这些类型本来是相同的？

编辑：自然同构？

看起来多态函数 Hask 是从函子 getConst :: forall a,b. Konst a b -> a 到常量函子 η : (Konst m) ⇒ Δm 的自然同构 Konst m 的候选者，即使我没有尚无法确定后者是否可在 Haskell 代码中表达。

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

相关参考资料

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

• StackOverflow，"Do all Type Classes in Haskell have a Category-Theoretic Analogue?"
• StackOverflow，"How are functors in Haskell related to functors in category theory?"
• 维基图书，Haskell/Category Theory

解决方法

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

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

Konst Int Bool

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

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。 （我们可以用单射类型家族来改善这个问题，但这只会让我们回到我们开始的同一个问题：问题恰恰是 const 函子不是单射的！）

对于现代 Haskell，没问题，这只是意味着你需要明确你正在使用的函子。 （可以说，无论如何，这通常是一件好事！）完整示例：

FunctorTyM f

输出：

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

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

,

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

附录。

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

,

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

type CF m a = m

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

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