20

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

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

如果这两个概念并不真正相关，只是名称相似，那么 Haskell 中是否使用了电梯（范畴论）？

4

2 回答 2

23

升降机和扩展的双重概念在 Haskell 中绝对使用，也许最突出的是 comonadicextend和monadic bind。（令人困惑的是，extend是电梯，而不是扩展。）comonadw让extend我们获取一个函数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

大多数Haskellers 更熟悉的是monad的bind( ) 的双重概念。给定一个函数and ，我们可以“扩展”我们的函数以获得一个函数。在 ASCII 艺术中：>>=ma -> m breturn :: a -> m areturnm a -> m b

a ---> m b
|
V
m a

给我们

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

（那A是一个箭头！）

所以是的, extendcould have been called lift, 并且bindcould have been called extend。至于Haskell's lift，我不知道他们为什么这么叫！

编辑：实际上，我再次认为，Haskell 的lifts 实际上是扩展。如果f是可应用的，并且我们有一个函数a -> b -> c，我们可以将这个函数组合pure :: c -> f c成一个函数a -> b -> f c。Uncurrying，这与 function 相同(a, b) -> f c。现在我们也可以通过 hit (a, b)withpure来获得一个函数(a, b) -> f (a, b)。现在，通过fmapingfst和snd，我们得到一个函数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实际上给了我们沿垂直箭头的水平箭头的延伸。

于 2014-07-21T03:11:15.613 回答
0

“提升”在函数式编程中多次出现，不仅在许多其他上下文中，fmap而且在许多其他上下文中。“举重”的例子包括：

  • fmap :: (a -> b) -> F a -> F bF函子在哪里
  • cmap :: (b -> a) -> F a -> F bF反函子在哪里
  • bind :: (a -> M b) -> M a -> M bM单子在哪里
  • ap :: F (a -> b) -> F a -> F bF应用函子在哪里
  • point :: (_ -> a) -> _ -> F aF指向函子在哪里
  • filtMap :: (a -> Maybe b) -> F a -> F bF可过滤函子在哪里
  • extend :: (M a -> b) -> M a -> M bMcomonad在哪里

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

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

在这些不同的情况下，函数类型不仅仅是简单的a -> b，而是具有某种“扭曲”的类型：例如a -> M bor F (a -> b)or or M a -> borF a -> F b等​​等。然而，每一次的规律都非常相似：扭曲的函数类型需要有恒等律和组合律，而扭曲的组合需要具有关联性。

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

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

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

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

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

这样，我们可以说“提升”很重要，并提供了范畴论在函数式编程中的应用。

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

于 2019-12-07T01:15:44.827 回答