【问题标题】:How are functors in Haskell related to functors in category theory?Haskell 中的函子与范畴论中的函子有何关系?
【发布时间】:2013-01-27 00:38:37
【问题描述】:

据我所知,仿函数是两个类别之间的映射,例如从 中的对象到 中的对象,其中 是类别。

在 Haskell 中有 Hask,其中对象是 Haskell 类型,而态射是 Haskell 函数。但是,Functor 类型类有一个函数fmap,它映射这些类型(因此它们是对象而不是类别本身):

fmap :: (a -> b) -> f a -> f b

f af b 都是 Hask 中的对象。这是否意味着 Haskell 中 Functor 的每个实例都是一个内函子,如果不是,Functor 真的代表一个函子吗?

我在这里缺少什么? Haskell 中的类型也是类别吗?

【问题讨论】:

    标签: haskell functor category-theory


    【解决方案1】:

    Functor 的实例指定了两件事:类型构造函数 F 类型为 * -> *,即从 Hask 对象到 Hask 对象的映射,以及类型为 (a -> b) -> (F a -> F b) 的函数,即,从 Hask 的箭头到 Hask 的箭头的映射与对象映射F 兼容。所以,是的,Functor 的所有实例都是内函子。在 Hackage 上有几种概括,例如Control.Categorical.Functor.

    【讨论】:

    • 你说 Hask 的箭头与对象映射 F 兼容。这是 Hask 的一个子类别吗?
    • @Zoidberg 是的,它是 Hask 的子类别,其对象是最外层类型构造函数为 F 的类型。
    • 我理解正确吗:理论上这些内函子不一定必须适用于类型为* -> *的类型,我的意思是函子可以将函数Int -> Char映射到函数String -> Double。据我了解,理论上函子适用于任何态射。但我想这不太实用。还是我在这里完全错了?
    • 我的思路:函子的定义:将对象映射到对象,将函数映射到函数(在Hask中)。所以潜在的一些仿函数可以将这个类别中的任何函数映射到这个类别中的任何其他函数。所以潜在地可以存在将一些Int -> Char映射到String -> Double的函子。 IE。 a -> bc -> d。或者这是假的?我知道 Functor 将 a -> b 映射到 F a -> F b,但是是否有一个仿函数可以在另一端不使用类型构造函数的情况下进行映射?同样,我的意思是至少在理论上。
    • @dimsuz 是的,这是允许的。当然,关于映射有一些 规则——特别是函数的映射必须与对象的映射兼容——但是您提出的特定建议还没有明显违反该规则。现代 Haskell 甚至几乎通过类型族使其成为可能;支持一流类型级函数的语言会很自然地支持它。
    【解决方案2】:

    是的,所有 Functor 实例都是 Hask 上的 endofunctors——事实上,所有 Hask 的 endofunctors 到一个适当的子类别,其对象是通过应用获得的类型特定类型的构造函数。该类型构造函数与 Functor 实例相关联,并提供对象的映射;态射的映射是fmap,它(因为我们只关心笛卡尔闭范畴上的内函子)本身就是Hask中的一个态射族。

    除了可以有 Functor 实例的函子之外,考虑其他函子确实是有意义的,例如 contravariant functors(从 Hask 到其相反的类别)。 the Arrow class中的arr函数也对应一个函子,从Hask的所有对象到与Hask的对象相同且其态射被描述的范畴Arrow 实例关联的类型构造函数。

    进一步的概括也是可能的(正如 Daniel Wagner 指出的那样),但使用起来会变得越来越尴尬。

    【讨论】:

      【解决方案3】:

      关于这一点的重要一点是,您真正想要的是 Hask丰富的函子,而不仅仅是普通的旧函子。 Hask 是笛卡尔封闭的(not really,但它努力做到这一点),因此它本身自然丰富。

      现在,丰富的 endofunctor 为您提供了一种限制那些在语言中实现的方法:丰富的仿函数 Hask -> Hask 是对象级别的函数( types)f a 和每对对象a, b Hask 中的态射 f : Hask(a,b) -> Hask (fa,fb)。当然,这只是fmap :: (a -> b) -> f a -> f b

      【讨论】:

        猜你喜欢
        • 1970-01-01
        • 1970-01-01
        • 2019-05-20
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        相关资源
        最近更新 更多