功能组合VS功能应用

Question

1. 谁能给出函数组合的例子？

2. 这是函数组合算子的定义？

   (.) :: (b -> c) -> (a -> b) -> a -> c
   f . g = \x -> f (g x)
   

这表明它需要两个函数并返回一个函数，但我记得有人用英语表达过类似的逻辑

男孩是人->阿里是男孩->阿里是人

1. 这个逻辑与函数组合有什么关系？
2. 函数应用和组合的强绑定是什么意思，哪个比哪个强？

请帮忙。

谢谢。

Answer 1

（编辑 1：我第一次错过了您问题的几个组成部分；请参阅我的答案底部。）

考虑这种陈述的方法是查看类型。您拥有的论证形式称为三段论；但是，我认为您记错了一些东西。有许多不同种类的三段论，据我所知，你的三段论并不对应于功能组合。让我们考虑一种三段论：

1. 如果外面晴天，我会很热。
2. 如果我热了，我会去游泳。
3. 所以，如果天气晴朗，我会去游泳。

这称为hypothetical syllogism。在逻辑上，我们可以这样写：让S代表命题“天气晴朗”，让H代表命题“我会变热” , 并让 W 代表“我要去游泳”这个命题。 α → β 表示“α 蕴含 β”，而写 ∴ 表示“因此”，我们可以翻译以上为：

1. S → H
2. H → W
3. ∴ S → W

当然，如果我们将 S、H 和 W 替换为任意 α，则此方法有效， β 和 γ。现在，这应该看起来很熟悉。如果我们把蕴含箭头→改为函数箭头->，就变成了

1. a -> b
2. b -> c
3. ∴a -> c

你瞧，我们有组合运算符类型的三个组成部分！要将其视为逻辑三段论，您可以考虑以下几点：

1. 如果我有一个a 类型的值，我可以产生一个b 类型的值。
2. 如果我有一个b 类型的值，我可以产生一个c 类型的值。
3. 因此，如果我有一个a 类型的值，我可以产生一个c 类型的值。

这应该是有道理的：在f . g 中，函数g :: a -> b 的存在告诉你前提1 为真，f :: b -> c 告诉你前提2 为真。因此，您可以得出结论，函数f . g :: a -> c 是其见证。

我不完全确定你的三段论翻译成什么。这几乎是modus ponens 的一个实例，但不完全是。 Modus ponens 论证采用以下形式：

1. 如果下雨，我会被淋湿的。
2. 下雨了。
3. 因此，我会弄湿的。

R 表示“下雨了”，W 表示“我会淋湿”，这给了我们逻辑形式

1. R → W
2. R
3. ∴ W

用函数箭头替换蕴含箭头给我们以下结果：

1. a -> b
2. a
3. ∴b

而这只是简单的函数应用，从($) :: (a -> b) -> a -> b的类型我们可以看出。如果你想把它看作一个逻辑论证，它可能是这种形式

1. 如果我有一个a 类型的值，我可以产生一个b 类型的值。
2. 我有一个a 类型的值。
3. 因此，我可以生成b 类型的值。

在这里，考虑表达式f x。函数f :: a -> b是命题1真实性的见证人；值x :: a是命题2真实性的见证；因此结果可以是b 类型，证明了结论。这正是我们从证明中发现的。

现在，您的原始三段论采用以下形式：

1. 所有男孩都是人类。
2. 阿里是个男孩。
3. 因此，阿里是人。

让我们把它翻译成符号。 Bx 将表示 x 是男孩； Hx 将表示 x 是人类； a 表示阿里；和∀x。 φ 表示 φ 对于 x 的所有值都为真。然后我们有

1. ∀x。 Bx → Hx
2. 巴
3. ∴ 哈

这几乎是 ponens，但它需要实例化 forall。虽然在逻辑上是有效的，但我不确定如何在类型系统级别解释它；如果有人想帮忙，我会全力以赴。一种猜测是像(forall x. B x -> H x) -> B a -> H a 这样的rank-2 类型，但我几乎可以肯定那是错误的。另一种猜测是更简单的类型，例如(B x -> H x) -> B Int -> H Int，其中Int 代表 Ali，但我几乎可以肯定它是错误的。再说一遍：如果你知道，也请告诉我！

最后一点。以这种方式看待事物 - 遵循证明和程序之间的联系 - 最终会导致 Curry-Howard isomorphism 的深层魔力，但这是一个更高级的主题。 （不过真的很酷！）

---

编辑 1：您还要求提供函数组合的示例。这是一个例子。假设我有一个人的中间名列表。我需要构建所有中间名首字母的列表，但要做到这一点，我首先必须排除每个不存在的中间名。很容易排除中间名为空的每个人；我们只是包括每个中间名不为空的filter (\mn -> not $ null mn) middleNames。同样，我们可以使用head 轻松获取某人的中间名首字母，因此我们只需要map head filteredMiddleNames 即可获取列表。换句话说，我们有以下代码：

allMiddleInitials :: [Char]
allMiddleInitials = map head $ filter (\mn -> not $ null mn) middleNames

但这是令人恼火的具体情况；我们真的想要一个中间初始生成函数。所以让我们把它变成一个：

getMiddleInitials :: [String] -> [Char]
getMiddleInitials middleNames = map head $ filter (\mn -> not $ null mn) middleNames

现在，让我们看一些有趣的东西。函数map 的类型为(a -> b) -> [a] -> [b]，由于head 的类型为[a] -> a，map head 的类型为[[a]] -> [a]。同样，filter 的类型为 (a -> Bool) -> [a] -> [a]，因此 filter (\mn -> not $ null mn) 的类型为 [a] -> [a]。因此，我们可以去掉参数，改为写

-- The type is also more general
getFirstElements :: [[a]] -> [a]
getFirstElements = map head . filter (not . null)

您会看到我们有一个额外的组合实例：not 的类型为 Bool -> Bool，null 的类型为 [a] -> Bool，所以 not . null 的类型为 [a] -> Bool：它首先检查给定的类型list 为空，然后返回是否不是。这次改造，顺便把函数改成了point-free style；也就是说，结果函数没有显式变量。

您还询问了“强绑定”。我认为您指的是. 和$ 运算符的优先级（也可能是函数应用程序）。在 Haskell 中，就像在算术中一样，某些运算符的优先级高于其他运算符，因此绑定更紧密。例如，在表达式1 + 2 * 3 中，它被解析为1 + (2 * 3)。这是因为在 Haskell 中，以下声明是有效的：

infixl 6 +
infixl 7 *

数字（优先级）越高，调用该运算符的越早，因此该运算符的绑定越紧密。函数应用程序实际上具有无限优先级，因此它绑定得最紧密：表达式f x % g y 将解析为(f x) % (g y) 对于任何运算符%。 .（组合）和$（应用程序）运算符具有以下固定性声明：

infixr 9 .
infixr 0 $

优先级范围从 0 到 9，所以这说明. 运算符比任何其他运算符（函数应用程序除外）绑定更多，而$ 绑定不那么紧。因此，表达式f . g $ h 将解析为(f . g) $ h；事实上，对于大多数运营商来说，f . g % h 将是 (f . g) % h，f % g $ h 将是 f % (g $ h)。 （唯一的例外是少数其他零或九优先级运算符。）