Haskell 中的`(a -> b) -> (c -> d)`?

`(a -> b) -> (c -> d)` in Haskell?

这是另一个 Haskell-through-through-category-theory 问题。

我们举一个简单而广为人知的例子。 fmap? 所以 fmap :: (a -> b) -> f a -> f b,忽略了 f 实际上是一个 Functor 的事实。据我了解,(a -> b) -> f a -> f b 只不过是 (a -> b) -> (f a -> f b) 语法糖 ;因此得出结论:

(1) fmap是函数产生函数。

现在,Hask 也包含函数,因此 (a -> b),特别是 (f a -> f b) 一个对象 的 Hask(因为 Hask 的对象是明确定义的 Haskell 类型 - a-ka 数学集合 - 并且确实存在类型 (a -> b) 的集合对于每个可能的 a,对?)。所以,再一次:

(2) (a -> b) 是 Hask 的对象。

现在奇怪的事情发生了:fmap,显然,是 Hask 的 态射 ,所以它是一个函数,接受另一个函数并将其转换为还有一个功能; 尚未应用最终功能

因此,从 (f a -> f b)f b 还需要一个 Hask 态射。对于类型 a 的每个项目 i 存在一个定义为 \f -> f (lift i) 的态射 apply_i :: (f a -> f b) -> f b,其中 lift i 是构建 f a 的一种方式特别是i里面。

另一种查看方式是 GHC 样式:(a -> b) -> f a -> f b。与我上面写的相反,(a -> b) -> f a 映射到 Hask 的常规对象。但是这样的观点与 Haskell 的基本公理相矛盾——没有多元函数,而是应用(curried)替代函数。


此时我想问:(a -> b) -> f a -> f b 应该是一个 (a -> b) -> (f a -> f b) -> f b,为了简单起见,还是我错过了一些非常非常重要的东西?

is (a -> b) -> f a -> f b suppose to be an (a -> b) -> (f a -> f b) -> f b, sugared for simplicity

没有。我认为你错过了什么,这不是你的错,只是一个非常特殊的情况 (a -> b) <b>-></b> (f a -> f b) 可以被称为 态射 与外部 (a <b>-></b> b) -> (f a <b>-></b> f b) 即可。 Functor class 的一般情况是(在伪语法中)

class (Category (──>), Category (~>)) => Functor f (──>) (~>) where
  fmap :: (a ──> b) -> f a ~> f b

因此,它将箭头表示为 ──> 的类别中的态射映射到类别 ~> 中的态射,但是这个态射映射本身只是一个 函数 。你的权利,在 Hask 中,函数箭头与态射箭头是同一类箭头,但从数学上讲,这是一个相当退化的场景。

fmap实际上是一个完整的态射。 Hask 中的态射总是从一个具体类型到另一个具体类型。如果函数具有具体的参数类型和具体的 return 类型,则可以将函数视为态射。 Int -> Int 类型的函数表示 Hask 中从 IntInt 的态射(实际上是自同态)。 fmap,但类型为 Functor f => (a -> b) -> f a -> f b。看不到具体的类型!我们只有类型变量和一个准运算符 => 需要处理。

考虑以下一组具体函数类型。

Int -> Int
Char -> Int
Int -> Char
Char -> Char

此外,考虑以下类型构造函数

[]
Maybe

[] 应用于 Int return 一种我们可以称为 List-of-Ints 的类型,但我们通常只调用 [Int]。 (当我开始学习仿函数时,最令人困惑的事情之一是我们没有单独的名称来指代各种类型构造函数产生的类型;输出只是由对其求值的表达式命名。)Maybe Int return就是我们刚才所说的类型,嗯,Maybe Int.

现在,我们可以像下面这样定义一堆函数

fmap_int_int_list :: (Int -> Int) -> [Int] -> [Int]
fmap_int_char_list :: (Int -> Char) -> [Int] -> [Char]
fmap_char_int_list :: (Char -> Int) -> [Char] -> [Int]
fmap_char_char_list :: (Char -> Char) -> [Char] -> [Char]
fmap_int_int_maybe :: (Int -> Int) -> Maybe Int -> Maybe Int
fmap_int_char_maybe :: (Int -> Char) -> Maybe Int -> Maybe Char
fmap_char_int_maybe:: (Char -> Int) -> Maybe Char -> Maybe Int
fmap_char_char_maybe :: (Char -> Char) -> Maybe Char -> Maybe Char

Hask中,每一个都是不同的态射,但是当我们在Haskell中定义它们时,有很多重复。

fmap_int_int_list f xs = map f xs
fmap_int_char_list f xs = map f xs
fmap_char_int_list f xs = map f xs
fmap_char_char_list f xs = map f xs
fmap_int_int_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_int_char_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_char_int_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_char_char_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)

f的类型不同,定义不一样,只有x/xs的类型不同。这意味着我们可以定义以下多态函数

fmap_a_b_list f xs = map f xs
fmap_a_b_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)

其中每个代表 Hask.

中的一组态射

fmap 本身是一个总称,我们用来指代所有多态函数所引用的特定于构造函数的态射。

除此之外,我们可以更好地理解 fmap :: Functor f => (a -> b) -> f a -> f b

给定fmap f,我们先看f的类型。例如,我们可能会发现 f :: Int -> Int,这意味着 fmap f 必须 return fmap_int_int_listfmap_int_int_maybe 之一,但我们不确定是哪个然而。因此,它 return 是类型 Functor f => (Int -> Int) -> f Int -> f Intconstrained 函数。一旦该函数应用于 [Int]Maybe Int 类型的值,我们最终将获得足够的信息来了解实际意味着哪个态射。

Now weird thing happens: fmap, obviously, is a morphism of the Hask, so it is a function, that takes another function and transform it to a yet another function; final function hasn't been applied yet.

Hence, one needs one more Hask's morphism to get from the (f a -> f b) to the f b. For each item i of type a there exists a morphism apply_i :: (f a -> f b) -> f b defined as \f -> f (lift i), where lift i is a way to build an f a with particular i inside.

范畴论中应用的概念以 CCC's - Cartesian Closed Categories 的形式建模。如果您具有自然双射 (X×Y,Z) ≅ (X,Y⇒Z),则类别是 CCC。

特别是这意味着存在自然变换(评估),其中 [Y,Z]:(Y⇒Z)×Y→Z,这样对于每个 g:X×Y→Z存在 g:X→(Y⇒Z) 使得 g = g×id;[Y,Z]。所以当你说,

Hence, one needs one more Hask's morphism to get from the (f a -> f b) to the f b.

你从 (f a -> f b)f b 的方式,或者使用上面的符号,从 (f a ⇒ f b) 是通过 [f a,f b]:(f a ⇒ f b) × f a → f b.

要牢记的另一点是,在范畴论中,“元素”不是原始概念。相反,一个元素是一个形式为 →X 的箭头,其中是终端对象。如果你取 X= 你有 (Y,Z) ≅ (×Y,Z) ≅ (,Y⇒Z)。也就是说,态射 g:Y→Z 与元素 g:→(Y⇒Z).

双射

在Haskell中这意味着函数正是箭头类型的“元素”。因此,在 Haskell 中,应用程序 h y 将通过在 y:→Y 上评估 h:→(Y⇒Z) 来建模。即(h)×y:→(Y⇒Z)×Y的评价,由组合(h)×y;[Y,Z]:→Z.

给出

为了完整起见,此答案侧重于各种评论中提到的一点,但其他答案没有提到。

The other way to see it is GHC-style: (a -> b) -> f a -> f b. On the contrast with what I've written above, (a -> b) -> f a is mapping to the regular object of the Hask.

类型签名中的

-> 是右结合的。既然如此,(a -> b) -> f a -> f b(a -> b) -> (f a -> f b) 实际上是一样的,在其中看到 (a -> b) -> f a 将是句法混淆。这与...没有什么不同

(++) :: [a] -> [a] -> [a]

... 并不意味着部分应用 (++) 会给我们一个 [a] 列表(相反,它会为我们提供一个在某些列表前面添加的函数)。

从这个角度来看,您提出的范畴论问题(例如,在 "need[ing] one more Hask's morphism to get from the (f a -> f b) to the f b" 上)是一个单独的问题,由 很好地解决。