在函数式编程的背景下，举升（lifting）与范畴论有何关系？

Question

看着Haskell文档，lifting似乎基本上是fmap的泛化，允许映射具有多个参数的函数。

然而，维基百科对lifting的解释完全不同，它用范畴中的态射来定义"lift"，以及它如何与范畴中的其他对象和态射相关联（这里我不会详细说明）。我猜如果我们考虑Cat（类别的范畴，因此使我们的态射函子化），那么这可能与Haskell情况相关，但是根据链接的文章，我无法看到这种范畴论上的提升如何与Haskell中的提升相关联，如果有的话。

如果这两个概念实际上没有关系，只是名字相似，那么lifting（范畴论）在Haskell中是否被使用？

- Nathan BeDell

Answer 1

在Haskell中，lift和扩展的二元概念是绝对常用的，可能最突出的是作为共范畴extend和单范畴bind的代表。 （令人困惑的是，extend是一个lift而不是一个extension。）一个共范畴w的extend可以让我们沿着extract :: w b -> b将函数w a -> b提升到w a -> w b的映射中。在ASCII艺术中，给定图表

        w b
         |
         V
w a ---> b

其中垂直箭头为提取，extend 给我们一个对角箭头（使图表可交）：

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

对于大多数 Haskell 程序员来说更为熟悉的是单子 m 的双重概念：绑定 (>>=)。给定一个函数 a -> m b 和 return :: a -> m a，我们可以沿着 return "扩展" 函数以获得一个函数 m a -> m b。在 ASCII 艺术中：

a ---> m b
|
V
m a

给我们

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

(那个箭头是箭头！)

因此，extend本来可以被称为lift，而bind本来可以被称为extend。至于Haskell的lifts，我不知道它们为什么会被叫做那样！

编辑：实际上，我想再次指出，Haskell的lifts实际上是扩展（extensions）。如果f是应用函子（applicative），并且我们有一个函数a -> b -> c，我们可以将这个函数与pure :: c -> f c组合，得到一个函数a -> b -> f c。去除柯里化，这就相当于一个函数(a，b) -> f c。现在我们还可以使用pure击中(a，b)，获得一个函数(a，b) -> f (a，b)。现在，通过对fst和snd进行fmap，我们得到两个函数f (a，b) -> f a和f (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 实际上给我们沿着垂直箭头的水平箭头的扩展。

- Evan Jenkins

---

+1 让我在第一、二、三次阅读时对这个答案的理解有多么少感到好笑。ASCII图表让它变得更加生动形象，我个人认为。 - Tom W

Answer 2

“Lifting”在函数式编程中经常出现，不仅在fmap中，在许多其他情况下也是如此。 “Liftings”的示例包括：

• 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 是一个余单子

其他例子包括适用的反函子、可过滤的反函子和共指函子。

所有这些类型签名在某种程度上都很相似：它们将在a和b之间映射一种函数到另一种函数。

在这些不同的情况下，函数类型不仅仅是a -> b，而是具有某种“扭曲”的类型：例如a -> M b或F (a -> b)或M a -> b或F a -> F b等。然而，每次定律都非常相似：扭曲的函数类型需要具有身份和组合法则，并且扭曲的组合需要是可结合的。

例如，对于适用函子，我们需要能够组合类型为F(a -> b)的函数。因此，我们需要定义一个特殊的“扭曲”恒等函数（pure id :: F(a -> a)）和一个“扭曲”的组合操作，称之为apcomp，其类型签名为F(a -> b) -> F(b -> c) -> F(a -> c)。这个操作需要具有恒等律和结合律。 ap操作需要具有恒等律和组合律（“扭曲恒等映射到扭曲恒等”，“扭曲组合映射到扭曲组合”）。

一旦我们通过所有这些示例并推导出定律，我们可以证明，如果我们通过“扭曲”操作来制定定律，则在所有情况下，定律都是相同的。

这是因为我们可以将所有这些操作都表述为范畴论中的函子。例如，对于应用函子，我们定义了两个类别：F-应用类别（对象为 a、b，... 等，态射为 F(a -> b)）和 F-lifted 类别（对象为 F a、F b，... 等，态射为 F a -> F b）。这两个类别之间的一个函子需要求出态射的 lifting，ap :: F(a -> b) -> F a -> F b。对于 ap 的法则完全等价于该函子的标准法则。

其他类型类的情况类似。我们需要在每种情况下定义类别、态射、组合操作、恒同态射和函子。一旦验证了所遵循的法则，我们将会看到每个类型类都有与之相关的一对类别和一个函子，使得类型类的法则等价于这些类别和函子的法则。

我们获得了什么？我们以相同的方式（作为范畴和函子的法则）制定了许多类型类的法则。这是一种伟大的思想经济：我们不需要每次都记住所有这些法则；只要记住每个类型类需要编写哪些范畴和哪些函子，只要类型类的方法可以归约为某种“扭曲提升”，就可以了。

通过这种方式，我们可以说，“提升”在函数式编程中非常重要，并提供了范畴论在应用方面的应用。

我已经做了一个关于这个主题的演示https://www.youtube.com/watch?v=Zau8CxsfxOo，并且我正在撰写一本新的免费书籍，其中将展示所有推导https://github.com/winitzki/sofp。

- winitzki