这是什么类型的数学：a -> b -> c答案

【问题标题】：What type of math is this: a -> b -> c这是什么类型的数学：a -> b -> c
【发布时间】：2011-07-23 22:00:34
【问题描述】：

在查看 Haskell 时，我经常会看到类似的类型声明：

a -> (b -> c)

我知道它描述了一个函数，该函数接受 a 类型的内容并返回一个新函数，该函数接受 b 类型的内容并返回 c 类型的内容。我也明白类型是关联的（编辑：我错了 - 请参阅下面的 cmets），因此可以像这样重写上面的内容以获得相同的结果：

(a -> b) -> c

这将描述一个函数，该函数接受 a 类型的东西和 b 类型的东西并返回 c 类型的东西。

我还听说您可以通过切换箭头来对函数进行补充（编辑：真的，我在这里寻找的词是双重的 - 请参阅下面的 cmets）：

a <- b <- c

我认为相当于

c -> b -> a

但我不确定。

我的问题是，这种数学的名称是什么？我想了解更多关于它的信息，这样我就可以用它来帮助我编写更好的程序。我有兴趣了解什么是互补函数，以及可以对类型声明执行哪些其他转换。

谢谢！

【问题讨论】：

a -> b -> c 和 a -> (b -> c) 采用 a 并返回一个（采用 b 并返回 c 的函数），即它们采用两个参数。 (a -> b) -> c 接受一个（接受一个a 并返回一个b 的函数）并返回一个c，即它们接受一个参数。所以它们不等价！

【解决方案1】：

类型声明不是关联的，a -> (b -> c) 不等同于 (a -> b) -> c。此外，您不能“切换”箭头，a <- b <- c 不是有效的语法。

在这种情况下，通常对关联性的引用是-> 它是right associative，这意味着a -> b -> c 被解释为a -> (b -> c)。

【讨论】：

【解决方案2】：

广义地说，这属于Lambda Calculus 的领域。

由于此符号与函数类型有关，type inference 您可能也会感兴趣。

（您对关联性所做的错误假设应该已经被其他答案充分澄清，所以我不会重申）

【讨论】：

另外，对偶函数的概念来自category theory，这对函数式程序员来说可能很有趣、有趣和有启发性。
二元论，没错，这就是我要找的词。我从我看过的关于它的视频中记错了。谢谢！
特别是，这是“类型化 lambda 演算”。在常规 lambda 演算中，只有一种“类型”。是的，它与范畴论有关，特别是与拓扑斯理论有关。（这是因为在范畴论中，对象和函数是分开的概念，但在 Topos 理论中，有一个函数的“内部”概念。
可以指定并说我们正在处理笛卡尔封闭的类别。

【解决方案3】：

a -> (b -> c)

和

(a -> b) -> c

在 Haskell 中是 not 等价的。这就是可以建立在范畴论中的类型论。

前者是一个函数，它接受a 类型的参数并返回b -> c 类型的函数。而后者是将a -> b 类型的函数作为参数并返回c 类型的值的函数。

函数的补码是什么意思？类型为a -> (b -> c) 的函数的反函数类型为(b -> c) -> a。

【讨论】：

【解决方案4】：

a->b->c 类型的函数，实际上是你所说的函数链，是 Currying 的示例

【讨论】：