(编辑1:我第一次漏掉了你问题的几个组成部分,请看我的回答底部。)
这种语句的思考方式是看类型。您拥有的参数形式称为“三段论”; 但是,我认为您记错了某些内容。有许多不同类型的三段论,而您的三段论据我所知并不对应于函数组合。 让我们考虑一种可以做到这一点的三段论:
- 如果天晴,我会感到热。
- 如果我感到热,我会去游泳。
- 因此,如果天晴,我会去游泳。
这被称为假设三段论。从逻辑术语来说,我们将其写成以下形式:让S表示主张“天晴”,让H表示主张“我会感到热”,让W表示主张“我会去游泳”。将α→ β表示为“a意味着b”,并将∴表示为“因此”,我们可以将上述内容翻译为:
- 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 arguments采用以下形式:
- 如果下雨了,我会淋湿。
- 现在正在下雨。
- 因此,我会淋湿。
将“它正在下雨”替换为R,“我会淋湿”替换为W,这给出了逻辑形式:
- R → W
- R
- ∴ W
用函数箭头替换条件箭头,我们得到以下内容:
a -> b
a
- ∴
b
这就是函数应用,可以从($) :: (a -> b) -> a -> b
的类型中看出。 如果您想将其视为逻辑论证,则可能具有以下形式:
- 如果我有一个类型为
a
的值,我可以生成一个类型为b
的值。 - 我有一个类型为
a
的值。 - 因此,我可以生成一个类型为
b
的值。
在这里,考虑表达式f x
。 函数f :: a -> b
是命题1真实性的证明; 值x :: a
是命题2真实性的证明; 因此结果可以是类型b
,证明了结论。 这正是我们从证明中发现的。
现在,您最初的三段论采用以下形式:
- 所有男孩都是人类。
- Ali是男孩。
- 因此,Ali是人类。
让我们将其翻译成符号。 Bx表示x是男孩;Hx表示x是人类;a表示Ali;并且∀x。φ表示φ对所有的x值都成立。然后我们有:
- ∀x。Bx→Hx
- Ba
- ∴Ha
这几乎是一种蕴含式,但它需要实例化forall。虽然逻辑上是有效的,但我不确定如何在类型系统级别上解释它;如果有人想帮忙,我很愿意听取建议。一个猜测是像 (forall x. B x -> H x) -> B a -> H a
这样的二阶类型,但我几乎确定那是错误的。另一个猜测可能是一个更简单的类型,类似于(B x -> H x) -> B Int -> H Int
,其中Int
代表Ali,但同样,我几乎确定它是错误的。再说一遍:如果你知道,请告诉我!
最后一点。以这种方式看待事物——遵循证明和程序之间的联系——最终会导致Curry-Howard同构的深层魔力,但这是一个更高级的主题。(它确实很酷!)
编辑1:你还要求一个函数组合的例子。这里有一个例子。假设我有一个人名字的中间名列表。我需要构建一个所有中间名首字母的列表,但为了做到这一点,我首先必须排除每个不存在的中间名。排除中间名为null的人很容易;我们只需使用filter (\mn -> not $ null mn) middleNames
来包括每个中间名不为null的人。同样,我们可以使用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]
。因此,我们可以去掉参数,而写成:
getFirstElements :: [[a]] -> [a]
getFirstElements = map head . filter (not . null)
你看到了一个有关组合函数的额外实例:not
的类型为Bool -> Bool
,null
的类型为[a] -> Bool
,因此 not . null
的类型为 [a] -> Bool
:它首先检查给定列表是否为空,然后返回其是否不是。顺便说一下,这种转换将函数改变为无参数样式;也就是说,所得到的函数没有显式变量。
你还问到了“强绑定”。我认为你指的是.
和$
运算符(可能还包括函数应用)的优先级。在Haskell中,就像在算术运算中一样,某些运算符比其他运算符具有更高的优先级,因此绑定更紧密。例如,在表达式1 + 2 * 3
中,这被解析为1 + (2 * 3)
。这是因为在Haskell中,以下声明生效:
infixl 6 +
infixl 7 *
数字越高(优先级越高),运算符就会更早地被调用,因此运算符绑定得更紧密。函数应用实际上具有无限的优先级,因此它绑定得最紧密:对于任何运算符%
,表达式f x%g y
将解析为(f x)%(g y)
。 .
(组合)和 $
(应用)运算符具有以下固定声明:
infixr 9 .
infixr 0 $
运算符的优先级范围从零到九,因此这意味着.
操作符比任何其他操作符(除了函数应用)都要更紧密地绑定,而$
则绑定得不太紧密。 因此,表达式f . g $ h
将解析为(f . g) $ h
;实际上,对于大多数运算符,f . g % h
将是(f . g) % h
,f % g $ h
将是f % (g $ h)
。(仅有少数罕见的零优先级或九优先级运算符除外。)
(.) f g x = f $ g x
。 - alternative