【问题标题】:How does lifting (in a functional programming context) relate to category theory?提升(在函数式编程环境中)与范畴论有何关系?
【发布时间】:2014-07-21 02:33:51
【问题描述】:

查看Haskell 文档,提升似乎基本上是fmap 的概括,允许映射具有多个参数的函数。

Wikipedia 关于提升的文章给出了不同的观点,但是,根据类别中的态射定义“提升”,以及它与类别中的其他对象和态射的关系(我不会给出详情在这里)。我想如果我们正在考虑 Cat (类别的类别,从而使我们的态射函子),这可能与 Haskell 的情况有关,但我看不出这种升力的类别理论概念如何与 Haskell 中的根据链接的文章,如果有的话。

如果这两个概念并不真正相关,只是名称相似,那么 Haskell 中是否使用了提升(范畴论)?

【问题讨论】:

    标签: haskell category-theory


    【解决方案1】:

    Lifts 和扩展的双重概念在 Haskell 中绝对使用,也许最突出的是在 comonadic extend 和 monadic bind 的幌子下。 (令人困惑的是,extend 是电梯,而不是扩展。)comonad wextend 让我们采用函数 w a -> b 并将其沿 extract :: w b -> b 提升以获取地图 w a -> w b。在ASCII艺术中,给定图表

            w b
             |
             V
    w a ---> b
    

    在垂直箭头是提取的地方,extend 给了我们一个对角箭头(使图表通勤):

         -> w b
        /    |
       /     V
    w a ---> b
    

    大多数 Haskeller 更熟悉的是 bind (>>=) 的双重概念,用于单子 m。给定一个函数a -> m breturn :: a -> m a,我们可以沿着return“扩展”我们的函数,得到一个函数m a -> m b。在 ASCII 艺术中:

    a ---> m b
    |
    V
    m a
    

    给我们

    a ---> m b
     |  __A
     V /
    m a
    

    (那个A是一个箭头!)

    所以是的,extend 可以被称为liftbind 可以被称为extend至于 Haskell 的 lifts,我不知道他们为什么这么叫!

    编辑:实际上,我再次认为,Haskell 的 lifts 实际上是扩展。如果f 是可应用的,并且我们有一个函数a -> b -> c,我们可以将这个函数与pure :: c -> f c 组合得到一个函数a -> b -> f c。 Uncurrying,这与函数(a, b) -> f c 相同。现在我们也可以用pure(a, b) 来得到一个函数(a, b) -> f (a, b)。现在,通过fmaping fstsnd,我们得到函数f (a, b) -> f af (a, b) -> f b,我们可以将它们组合起来得到函数f (a, b) -> (f a, f b)。与我们之前的pure 组合得到(a, b) -> (f a, f b)。呸!回顾一下,我们有 ASCII 艺术图

      (a, b) ---> f c
        |
        V
    (f a, f b)
    

    现在liftA2 给了我们一个函数(f a, f b) -> f c,我不会画它,因为我厌倦了制作糟糕的图表。但重点是,图表是通勤的,所以liftA2 实际上为我们提供了水平箭头沿垂直箭头的延伸。

    【讨论】:

    • +1 让我在第一次、第二次和第三次传球时对这个答案知之甚少而发笑。 ASCII 图表做到了,恕我直言。
    【解决方案2】:

    “提升”在函数式编程中多次出现,不仅在 fmap 中,而且在许多其他上下文中。 “提升”的示例包括:

    • fmap :: (a -> b) -> F a -> F b 其中F 是函子
    • cmap :: (b -> a) -> F a -> F b 其中F 是一个反函子
    • bind :: (a -> M b) -> M a -> M b 其中M 是一个单子
    • ap :: F (a -> b) -> F a -> F b 其中F 是一个应用函子
    • point :: (_ -> a) -> _ -> F a 其中F 是一个指向函子
    • filtMap :: (a -> Maybe b) -> F a -> F b 其中F 是可过滤函子
    • extend :: (M a -> b) -> M a -> M b 其中M 是共胞

    其他示例包括应用反函子、可过滤反函子和共指向函子。

    所有这些类型签名在一个方面是相似的:它们将ab 之间的一种函数映射到ab 之间的另一种函数。

    在这些不同的情况下,函数类型不仅仅是a -> b,而是具有某种“扭曲”类型:例如a -> M bF (a -> b)M a -> bF a -> F b 等等。但是,每一次的规律都非常相似:twisted 函数类型需要有恒等律和组合律,并且twisted 组合需要具有关联性。

    例如,对于应用函子,我们需要能够组合F (a -> b) 类型的函数。所以我们需要定义一个特殊的“扭曲”标识函数(pure id :: F (a -> a))和一个“扭曲”组合操作,称为apcomp,类型签名F (a -> b) -> F (b -> c) -> F (a -> c)。这个操作需要有恒等律和结合律。 ap 操作需要有恒等式和组合律(“扭曲的恒等映射到扭曲的恒等”和“扭曲的组合映射到扭曲的组合”)。

    一旦我们通过所有这些例子并推导出定律,我们就可以证明,如果我们通过“扭曲”运算来制定定律,那么这些定律在所有情况下都是相同的。

    这是因为我们可以将所有这些操作表述为范畴论意义上的函子。例如,对于应用函子,我们定义了两个类别:F-应用类别(对象ab,...,态射F(a -> b))和F-提升类别(对象F a,@ 987654356@, ..., 态射F a -> F b)。这两个类别之间的函子要求我们提升态射,ap :: F(a -> b) -> F a -> F bap 的定律完全等同于该函子的标准定律。

    类似的参数适用于其他类型类。我们需要在每种情况下定义类别、态射、组合操作、恒等态射和函子。一旦我们验证了这些规律成立,我们就会看到这些类型类中的每一个都有一对关联的类别和它们之间的函子,因此类型类的规律等价于这些类别和函子的规律。

    我们得到了什么?我们以相同的方式制定了许多类型类的定律(如范畴和函子的定律)。这是一个伟大的思想经济:我们不需要每次都记住所有这些定律;我们可以只记住每个类型类需要写下哪些类别和哪些函子,只要类型类的方法可以简化为某种“扭曲提升”即可。

    通过这种方式,我们可以说“提升”很重要,并提供了类别理论在函数式编程中的应用。

    我已经对此进行了演示,https://www.youtube.com/watch?v=Zau8CxsfxOo 我正在编写一本新的免费书籍,其中将显示所有推导。 https://github.com/winitzki/sofp

    【讨论】:

      猜你喜欢
      • 2013-01-27
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 2012-07-28
      • 1970-01-01
      相关资源
      最近更新 更多