Как внешняя стратегия оценки оценивает частичное применение функции и применение функции с каррированием

Question

Программирование в Хаскеле Хаттоном говорит

При оценке выражения в каком порядке следует выполнять сокращения? Одна из распространенных стратегий, известная как внутренняя оценка, состоит в том, чтобы всегда выбирать переопределение, которое является самым внутренним, в том смысле, что оно не содержит других переопределений. Если существует более одного внутреннего переопределения, условно мы выбираем тот, который начинается в крайней левой позиции в выражении.

Еще одна распространенная стратегия оценки выражения, двойственного по отношению к внутреннему, состоит в том, чтобы всегда выбирать переопределение, которое является наиболее внешним, в том смысле, что оно не содержится ни в одном другом переопределении. Если существует более одного такого переопределения, то, как и ранее, мы выбираем то, что начинается с крайней левой позиции. Не удивительно, что эта стратегия оценки известна как внешняя оценка.

При частичном применении функции, например, 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 не кортеж типа (Int, Int),

В результате происходит уменьшение выражения mult (3,4) в том смысле, который подразумевает Хаттон, то же самое, используете ли вы внешнее или внутреннее сокращение. Здесь есть только один redex/ приложение, приложение mult в (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

Это потому, что применение ((\x -> \y -> x * y) 3) в 4 в строке (1), хотя это самое внешнее приложение, это не переопределение. Это не может быть уменьшено, потому что вещь применяется ((\x -> \y -> x * y) 3) не лямбда-выражение. (Это применение лямбда-выражения к аргументу.)

Следовательно, вопреки первому появлению, в строке (1) есть только один переопределение, и самые внутренние и внешние стратегии сокращения выбирают один и тот же переопределение.