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

Question

我知道Haskell中的许多名字都是受到范畴理论术语的启发，我正试图准确地理解类比的起点和终点。

我已经知道由于一些关于严格/懒惰和seq的技术细节，hask不（一定）是一个类别，但现在让我们先把那个放在一边。为了清楚起见,

• hask的对象是具体类型，即kind*的类型。这包括像int->[Char]这样的函数类型，但不包括像Maybe::*->*这样需要类型参数的函数类型。但是，具体类型可能是Int::*属于hask。类型构造函数/多态函数更像是自然转换（或从hask到自身的其他更一般的映射），而不是态射。
hask的态射是Haskell函数。对于两种具体类型 A和 B，HOM-集 HOM(A,B)是签名为 A->B的函数集合。
• 函数组成由f给出。G。如果我们担心严格性，我们可以重新定义合成，使之严格，或者在定义函数的等价类时小心。

我不认为上面的技术细节与我下面的困惑有任何关系。我想我理解它的意思是说functor的每个实例都是hask类别中的endofunctor。也就是说，如果我们

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实例可能对应于从hask到hask的一个函数，其方式如下：

>

在hask中给每个具体类型a分配具体类型Maybea

对于hask中的每个态射f::a->b，我们分配给发送nothing nothing和Just x Just(fx)的态射Maybe a->mayb。

范畴C上的常量（endo）函子是一个函子C:C,它将范畴C的每个对象映射到固定对象C∈C,并且C的每个态射映射到固定对象的恒等式态射ID_C:C。

请考虑data.functor.const。为了清楚起见，我将在这里重新定义它，区分类型构造函数const::*->*->*和数据构造函数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显示为const m a，由于多态性
• 在右侧，const v显示为const m b，由于多态性

但是，如果我们试图把konst m::*->*看作范畴理论意义上的常数函子，我的理解就会崩溃。

>

固定对象是什么？类型构造函数konst m采用一些具体类型a并给出一个konst ma，至少从表面上看，对于每个a都是不同的具体类型。我们确实希望将每个类型A映射到固定类型M。

根据类型签名，fmap取一个f::a->b并给出一个Konst m a->Konst m b。如果konst m类似于常数函子，则fmap将需要将每个态射发送到固定类型m上的同一性态射id::m->m。

所以，下面是我的问题：

>

Haskell的const函子在什么方面与范畴理论中的常数函子类似？

如果这两个概念不等价，那么用Haskell代码来表达范畴理论的常量函子（称它为simpleconst)有可能吗？我快速尝试了一下，遇到了与多态wrt幻象类型相同的问题，如下所示：

data SimpleKonst a = SimpleConst Int

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

如果#2的答案是肯定的，如果是，那么在范畴理论意义上，这两个哈斯克尔函数是以什么方式相关联的呢？也就是说，在Haskell中，simpleconst是const，就像常量函子在范畴理论中是__？__一样？

幻象类型是否会对将hask想成一个类别造成问题？我们是否需要修改hask的定义，以使对象实际上是类型的等价类，否则，如果没有幻影类型参数的存在，这些类型将是相同的？

它看起来像多态函数getconst::forall a,b。Konst a b->a是从函子Konst m到常数函子的自然同构 的候选者，尽管我还不能确定后者是否可用Haskell代码表示。

其自然转变规律为_x=(Konst m f）。？y。我很难证明这一点，因为我不知道如何正式地解释将(Const v)从类型konst m a转换为konst m b的原因，而不是说“存在双射！”。

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

• StackOverflow,“Haskell中的所有类型的类都有一个范畴理论的类比吗？”
• StackOverflow,“Haskell中的函子与范畴理论中的函子有何关系？”
• 维基图书，Haskell/类别理论




Answer 1

我们在这里遇到的问题是，从数学上讲，一个函子是一对相依的对，但它的一边(type->type映射）位于Haskell的类型级世界，而另一边((a->b)->fa->fb映射）位于值级世界。哈斯克尔没有一种方法来表达这样的对。functor类通过只允许类型构造函数作为type->type映射来绕过这个限制。
这样做的原因是类型构造函数是唯一的，即可以通过Haskell的typeclass机制为每一个构造函数分配一个定义良好的态射映射。但另一方面是，结果总是唯一的，因此最终出现的情况是，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来html" target="_blank">编译-这是因为不能从functortym f推断出f。（我们可以用内射类型族对此进行改进，但这只会使我们回到我们开始讨论的同一个问题：问题恰恰是常量函子不是内射的！）

对于modern Haskell，这是可以的，它只是意味着您需要明确地说明您使用的函数。（按理说，这往往是一件好事！）完整示例：

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