函数组合与函数应用

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

2. 这就是函数复合运算符的定义？

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

这表明它需要两个函数并返回一个函数，但我记得有人用英语表达了逻辑，例如

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

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

请帮忙。

Thanks.

(Edit 1:我第一次错过了你问题的几个组成部分；请参阅我的答案的底部。）

思考此类语句的方法是查看类型。你所拥有的论证形式称为三段论。但是，我认为你记错了一些事情。三段论有很多种，据我所知，你的三段论并不对应于函数组合。让我们考虑一种三段论：

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

这被称为假设三段论 http://en.wikipedia.org/wiki/Hypothetical_syllogism。用逻辑术语来说，我们可以这样写：S代表命题“外面阳光明媚”，令H代表命题“我会变热”，并让W代表“我要去游泳”的主张。写作α → β for "α暗示β”，并将“因此”写为 ∴，我们可以将上面的内容翻译为：

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

当然，如果我们更换S, H, and W与任何任意的α, β, and γ。现在，这看起来应该很熟悉。如果我们将蕴涵箭头→改为函数箭头->，这变成了

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是一个见证人。

我不完全确定你的三段论意味着什么。这几乎是一个例子前件 http://en.wikipedia.org/wiki/Modus_ponens，但不完全是。后件论证采用以下形式：

1. 如果下雨的话，我就会被淋湿。
2. 正在下雨。
3. 所以，我会被淋湿。

Writing 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. Ba
3. ∴ Ha

这几乎是肯定的做法，但它需要实例化 forall。虽然逻辑上有效，但我不确定如何在类型系统级别解释它；如果有人想帮忙，我洗耳恭听。一种猜测是 2 级类型，例如(forall x. B x -> H x) -> B a -> H a，但我几乎可以肯定这是错误的。另一种猜测是更简单的类型，例如(B x -> H x) -> B Int -> H Int, where Int代表阿里，但我几乎可以肯定这是错误的。再次强调：如果你知道，也请告诉我！

最后一点。以这种方式看待事物——遵循证明和程序之间的联系——最终会带来深刻的魔力库里-霍华德同构 http://en.wikipedia.org/wiki/Curry-Howard_isomorphism，但这是一个更高级的主题。 （不过，这真的很酷！）

Edit 1:您还要求提供函数组合的示例。这是一个例子。假设我有一个人们的中间名列表。我需要构建所有中间名缩写的列表，但要做到这一点，我首先必须排除每个不存在的中间名。很容易排除所有中间名为空的人；我们刚刚include每个中间名是not空与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, and null有类型[a] -> Bool, so not . null有类型[a] -> Bool：它首先检查给定列表是否为空，然后返回是否为空isn't。顺便说一下，这个转换将函数变成了无点风格 http://www.haskell.org/haskellwiki/Pointfree;也就是说，结果函数没有显式变量。

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

infixl 6 +
infixl 7 *

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

infixr 9 .
infixr 0 $

优先级范围从零到九，所以这说明的是.操作符绑定more比任何其他应用程序都紧密（函数应用程序除外），并且$ binds less紧紧。因此，表达式f . g $ h将解析为(f . g) $ h;事实上，对于大多数运营商来说，f . g % h将(f . g) % h and f % g $ h将f % (g $ h)。 （唯一的例外是极少数其他零或九个优先级运算符。）