6
  1. 任何人都可以举出功能组合的例子吗？

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

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

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

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

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

请帮忙。

谢谢。

4

1 回答 1

20

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

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

  1. 如果外面阳光明媚，我会很热。
  2. 如果我觉得热，我会去游泳。
  3. 因此，如果天气晴朗，我会去游泳。

这称为假设三段论。在逻辑上，我们可以这样写：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. 如果我有一个 type 的值a，我可以产生一个 type 的值b。
  2. 如果我有一个 type 的值b，我可以产生一个 type 的值c。
  3. 因此，如果我有一个 type 的值a，我可以产生一个 type 的值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. 如果我有一个 type 的值a，我可以产生一个 type 的值b。
  2. 我有一个 type 的值a。
  3. 因此，我可以产生一个 type 的值b。

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

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

  1. 所有的男孩都是人。
  2. 阿里是个男孩。
  3. 所以，阿里是人。

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

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

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

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

编辑 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有 type (a -> Bool) -> [a] -> [a]，所以filter (\mn -> not $ null mn)有 type [a] -> [a]。因此，我们可以去掉参数，而是写

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

你会看到我们有一个额外的组合实例：not有 type Bool -> Bool，null有 type [a] -> Bool，所以not . null有 type [a] -> Bool：它首先检查给定列表是否为空，然后返回是否不是。顺便说一下，这种转换将函数更改为无点样式；也就是说，结果函数没有显式变量。

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

infixl 6 +
infixl 7 *

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

infixr 9 .
infixr 0 $

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

于 2010-06-25T09:05:53.077 回答