最外部的评估策略如何评估功能的部分应用和咖喱函数的应用

Question

赫顿在Haskell编程说

计算表达式时，应以什么顺序执行归约？一种通用策略（称为 最内层评估）是始终选择最内层的Redex，因为它不包含其他Redex。如果最里面的redex不止一个，按照惯例，我们选择一个从表达式最左边的位置开始的redex。

对表达式进行评估的另一种常见策略是对最内层的评估，它总是选择最外层的Redex，因为它不包含在其他Redex中。如果有多个这样的redex，则像以前一样，我们选择从最左边开始的那个。毫不奇怪，这种评估策略被称为 最外部评估。

在部分应用功能时，例如mult(3)(4)，其中mult定义为

mult    ::  (Int,Int)   ->  Int
mult    (x,y)   =   x   *   y

最内层的评估将首先评估mult(3)为\y->3*y，然后评估(\y->3*y)4。最外部的评估将如何评估mult(3)(4)？

在应用咖喱函数时，例如mult'(3)(4)，其中

mult'   ::  Int ->  Int ->  Int
mult'   x   =   \y  ->  x   *   y

最内层的评估将首先评估mult'(3)为\y->3*y，然后评估(\y->3*y)4。最外部的评估将如何评估mult'(3)(4)？

Answer 1

唯一明智的解释方式是：

mult :: (Int, Int) -> Int
mult (x,y) = x * y

在您更大的问题的上下文中，它是一个采用元组类型的单个参数的一元函数(Int, Int)。因此，mult不能部分应用。特别地，mult(3)这没有任何意义，因为3它不是type的元组(Int, Int)。

结果，mult (3,4)无论您使用最外面的还是最里面的减少，Hutton所表示的表达式的减少都是相同的。这里只有一个redex / application，multto 的应用(3,4)，以及最外面和最里面的减少都将减少：

mult (3,4)
=>  3 * 4
=>  12

对于功能：

mult' :: Int -> Int -> Int
mult' x y = x * y

或等效地：

mult' = \x -> (\y -> x * y)

表达式mult' 3 4或等效形式(mult' 3) 4经历的最内层归约为：

(mult' 3) 4
= ((\x -> (\y -> x * y)) 3) 4
=> (\y -> 3 * y) 4
=> 3 * 4
=> 12

奇怪的是，最外面的减少以完全相同的方式进行：

(mult' 3) 4
= ((\x -> (\y -> x * y)) 3) 4     -- (1)
=> (\y -> 3 * y) 4
=> 3 * 4
=> 12

这是因为第（1）行中((\x -> \y -> x * y) 3)to 4的应用程序是最外层的应用程序，而不是redex。它不能减少，因为要应用的东西((\x -> \y -> x * y) 3)不是lambda表达式。（这是一个lambda表达式应用于参数的方法。）

因此，与首次出现相反，第（1）行中只有一个redex，并且最内部和最外部的归约策略选择相同的redex。