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

html5 • • 问答

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

类别 Hask

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

  • 的对象Hask是具体类型，即 kind 的类型*。这包括像 那样的函数类型Int -> [Char]，但不包括像Maybe :: * -> *. 但是，具体类型Maybe Int :: *属于Hask. 类型构造函数/多态函数更像是自然变换（或其他更一般的映射Hask到自身），而不是态射。
  • 的态射Hask是 Haskell 函数。对于两个具体类型Aand B，hom-setHom(A,B)是具有签名的函数集A -> B。
  • 函数组合由 给出f . g。如果我们担心严格性，我们可能会将组合重新定义为严格的，或者在定义函数的等价类时要小心。

Functors 是 Endofunctors Hask

我认为上面的技术细节与我下面的困惑没有任何关系。我想我理解它的意思是说 的每个实例Functor都是类别中的一个内函子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 上的常数（内）函子是一个函子?c : C ? C，将范畴 C 的每个对象映射到一个固定对象，c?C并将 C 的每个态射映射到固定对象的恒等态射id_c : c ? c。

这 Const Functor

考虑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显示为 a Konst m a，由于多态性，这是可以的
  • 在右侧，Const v显示为 a Konst m b，由于多态性，这是可以的

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

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

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

问题

所以，这里是我的问题：

  1. Const如果有的话，Haskell 的函子与范畴论中的常数函子有何相似之处？

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

data SimpleKonst a = SimpleConst Int

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

  1. 如果#2 的答案是肯定的，如果是，那么这两个 Haskell 函数在范畴论意义上以何种方式相关？也就是说，在 Haskell 中的SimpleConsttoConst就像常数函子__?__在范畴论中的to 一样？

  2. 幻像类型是否会给Hask像类别一样思考带来问题？我们是否需要修改 的定义，Hask以便对象真的是类型的等价类，如果没有幻像类型参数的存在，这些类型将是相同的？

编辑：自然同构？

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

自然变换定律是?_x = (Konst m f) . ?_y。我很难证明它，因为我不知道如何正式推理 a(Const v)从类型Konst m a到的转换Konst m b，而不是挥手说“存在双射！”。

相关参考资料

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

  • StackOverflow，“Haskell 中的所有类型类都具有范畴论类比吗？”
  • StackOverflow，“Haskell 中的函子与范畴论中的函子有什么关系？”
  • WikiBooks、Haskell/范畴论

回答

我们在这里遇到的问题是，函子在数学上是一对依赖对，但它的一侧（Type -> Type映射）位于 Haskell 的类型级世界中，而另一侧（(a -> b) -> f a -> f b映射）位于值级世界中. Haskell 没有办法表达这样的对。在Functor类的招数绕过这个限制的方式，只允许类型构造的Type -> Type映射。

这有帮助的原因是类型构造器是唯一的，即它们中的每一个都可以通过 Haskell 的类型类机制分配一个明确定义的态射映射。但另一方面，结果总是独一无二的，所以你最终会遇到技术上不同但同构的类型。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无法从FunctorTyM f. （我们可以用单射类型家族来改善这个问题，但这只会让我们回到我们开始的同一个问题：问题正是 const 函子不是单射的！）

使用现代 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)

回答

  1. 问：如果有的话，Haskell 的 Const 函子与范畴论中的常数函子有什么相似之处？
    A.Const a b将 ant 类型发送b到与 同构的类型a，而不是a像范畴论定义那样将其发送到。这没什么大不了的，因为同构对象是“真正相同的对象”。
  2. 问：如果这两个概念不等价，是否甚至可以SimpleConst在 Haskell 代码中表达范畴论常数函子（称其为）？
    A. 它们并不完全等价，但它们等价于同构，这已经足够好了。如果您想要精确等价，那么这取决于“在代码中表达函子”的确切含义。让我们考虑恒等函子，因为它比 Const 简单一些。你可以只写一个类型别名：type Id a = a并且相关的态射就是id. 如果你想Functor为 this编写一个实例Id，那么不，你不能在 Haskell 中这样做，因为你不能为类型别名编写类实例（也许在其他类似的语言中你可以这样做）。
  3. 问：[I]n 这两个 Haskell 函数在范畴论意义上以何种方式相关？
    答：没有的范畴论const的仿函数。每个对象都有一个const 函子。HaskellConst a与这样一个与 object 关联的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是不同但同构的对象。

以上是Haskell的“Const”函子是否类似于范畴论中的常数函子？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>