函数构成 AND 函数应用

Question

有没有人可以举出函数组合的例子？

这是函数组合运算符的定义？

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

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

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

这个逻辑与函数组合有什么关系？

函数应用和组合的强绑定(bind)是什么意思，哪个绑定(bind)比另一个强？

请帮忙。

谢谢。

Answer 1

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

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

如果外面是晴天，我会很热。

如果我热了，我就去游泳。

因此，如果天气晴朗，我就去游泳。

这称为 hypothetical syllogism .在逻辑上，我们可以这样写:让 S 代表命题“天气晴朗”，让 H 代表命题“我会变热”，让 W 代表命题“我会去游泳” .将 α → β 写为“α 意味着 β”，将 ∴ 写为“因此”，我们可以将上述转化为:

S → H

H → W

∴ S → W

当然，如果我们用任意的 α、β 和 γ 替换 S、H 和 W，这会起作用。现在，这应该看起来很熟悉。如果我们将蕴涵箭头 → 改为函数箭头 -> ，这变成

a -> b

b -> c

∴ a -> c

瞧，我们有组合运算符类型的三个组件!要将其视为逻辑三段论，您可以考虑以下内容:

如果我有一个类型为 a 的值, 我可以产生一个 b 类型的值.

如果我有一个类型为 b 的值, 我可以产生一个 c 类型的值.

因此，如果我有一个 a 类型的值, 我可以产生一个 c 类型的值.

这应该是有道理的:在 f . g ，存在函数 g :: a -> b告诉你前提 1 为真，并且 f :: b -> c告诉你前提 2 是正确的。因此，您可以得出最后的语句，函数 f . g :: a -> c 对此进行了总结。是证人。

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

如果下雨，我就会淋湿。

正在下雨。

因此，我会湿透的。

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

R → W

电话

∴ W

用函数箭头替换蕴涵箭头给我们以下内容:

a -> b

a

∴ b

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

如果我有一个类型为 a 的值, 我可以产生一个 b 类型的值.

我有一个类型为 a 的值.

因此，我可以生成类型为 b 的值.

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

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

所有的男孩都是人。

阿里是个男孩。

因此，阿里是人。

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

∀x。 Bx → Hx

巴

∴哈

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

还有最后一点。以这种方式看待事物——遵循证明和程序之间的联系——最终会导致 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 : 它首先检查给定的列表是否为空，然后返回是否为空。顺便说一下，这个转换把函数改成了 point-free style ;也就是说，结果函数没有显式变量。

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

infixl 6 +
infixl 7 *

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

infixr 9 .
infixr 0 $

优先级范围从 0 到 9，所以这意味着 .运算符比任何其他运算符绑定(bind)得更紧密(函数应用程序除外)，并且 $结合不那么紧密。因此，表达式 f . g $ h将解析为 (f . g) $ h ;事实上，对于大多数运营商来说， f . g % h将是 (f . g) % h和 f % g $ h将是 f % (g $ h) . (唯一的异常(exception)是少数其他零或九个优先运算符。)