Эта-конверсия меняет семантику на строгом языке

Question

Возьмите этот код OCaml:

let silly (g : (int -> int) -> int) (f : int -> int -> int) =
        g (f (print_endline "evaluated"; 0))

silly (fun _ -> 0) (fun x -> fun y -> x + y)

Он печатает evaluated и возвращает 0.Но если я разверну f, чтобы получить g (fun x -> f (print_endline "evaluated"; 0) x), evaluated больше не печатается.

То же самое относится и к этому SML-коду:

fun silly (g : (int -> int) -> int, f : int -> int -> int) : int =
        g (f (print "evaluated" ; 0));

silly ((fn _ => 0), fn x => fn y => x + y);

С другой стороны,этот код на Haskell не печатается evaluated даже со строгой прагмой:

{-# LANGUAGE Strict #-}

import Debug.Trace

silly :: ((Int -> Int) -> Int) -> (Int -> Int -> Int) -> Int
silly g f = g (f (trace "evaluated" 0))

main = print $ silly (const 0) (+)

(хотя я могу сделать это, используя seq, что для меня имеет смысл)

Хотя я понимаю, что OCaml и SML теоретически делают правильные вещи, есть ли практическая причина предпочесть такое поведение "более ленивому"?Эта-сокращение является распространенным инструментом рефакторинга, и я полностью боюсь использовать его на строгом языке.Я чувствую, что должен параноически все это расширять, просто потому, что в противном случае аргументы для частично примененных функций могут быть оценены, когда они не должны.Когда полезно «строгое» поведение?

Почему и как Haskell ведет себя по-разному под прагмой Strict?Есть ли какие-либо ссылки, с которыми я могу ознакомиться, чтобы лучше понять пространство дизайна и плюсы и минусы существующих подходов?

Answer 1

Что касается вашего последнего вопроса (почему Haskell делает это), причина, по которой «Strict Haskell» ведет себя иначе, чем действительно строгий язык, заключается в том, что расширение Strict не меняет модель оценки с ленивой на строгую. Он просто делает подмножество привязок в «строгие» привязки по умолчанию, и только в ограниченном смысле Хаскелла принуждения оценки к нормальной форме слабой головы. Кроме того, это влияет только на привязки, сделанные в модуле с включенным расширением; это не оказывает обратного влияния на привязки, сделанные в других местах. (Более того, как описано ниже, строгость не вступает в силу при частичном применении функции. Функция должна быть полностью применена, прежде чем какие-либо аргументы будут принудительными.)

В вашем конкретном примере на Haskell я считаю, что единственный эффект расширения Strict заключается в том, что вы явно написали следующие шаблоны взрыва в определении silly:

silly !g !f = g (f (trace "evaluated" 0))

Это не имеет никакого другого эффекта. В частности, он не делает const или (+) строгими в своих аргументах, а также не изменяет семантику приложений функций, чтобы сделать их нетерпеливыми.

Таким образом, когда print навязывает термин silly (const 0) (+), единственным эффектом является оценка его аргументов для WHNF как части приложения функции silly. Эффект похож на запись (в не-Strict Haskell):

let { g = const 0; f = (+) } in g `seq` f `seq` silly g f

Очевидно, что принуждение g и f к их WHNF (которые являются лямбдами) не будет иметь никакого побочного эффекта, и когда применяется silly, const 0 все еще ленив в своем оставшемся аргументе, итоговый термин выглядит примерно так:

(\x -> 0) ((\x y -> <defn of plus>) (trace "evaluated" 0))

(что следует интерпретировать без расширения Strict - здесь все ленивые привязки), и здесь нет ничего, что могло бы вызвать побочный эффект.

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

{-# LANGUAGE Strict #-}

import Debug.Trace

myConst :: a -> b -> a
myConst x y = x

myPlus :: Int -> Int -> Int
myPlus x y = x + y

silly :: ((Int -> Int) -> Int) -> (Int -> Int -> Int) -> Int
silly g f = g (f (trace "evaluated" 0))

main = print $ silly (myConst 0) myPlus

это все равно не напечатало бы "оценено". Это связано с тем, что при оценке silly, когда строгая версия myConst вынуждает свой второй аргумент, этот аргумент является частичным применением строгой версии myPlus, и myPlus не будет форсировать какую-либо его аргументы, пока он не будет полностью применен.

Это также означает, что если вы измените определение myPlus на:

myPlus x = \y -> x + y   -- now it will print "evaluated"

тогда вы сможете в значительной степени воспроизвести поведение ML. Поскольку myPlus теперь полностью применен, он заставит свой аргумент, и это выведет «оцененный». Вы можете снова подавить это расширение eta f в определении silly:

silly g f = g (\x -> f (trace "evaluated" 0) x)  -- now it won't

потому что теперь, когда myConst заставляет свой второй аргумент, этот аргумент уже находится в WHNF (потому что это лямбда), и мы никогда не доберемся до применения f, полного или нет.

В конце концов, я бы не стал слишком серьезно относиться к "Haskell плюс расширение Strict и небезопасным побочным эффектам, таким как trace", как к хорошей точке в области дизайна. Его семантика может быть (едва) последовательной, но они, конечно, странные. Я думаю, что единственный серьезный вариант использования - это когда у вас есть некоторый код, семантика которого «очевидно» не зависит от ленивых и строгих вычислений, но где производительность будет улучшена большим количеством форсирования. Затем вы можете просто включить Strict для повышения производительности, не задумываясь.

Answer 2

Чтобы ответить на техническую часть вашего вопроса, eta-преобразование также меняет значение выражений в ленивых языках, вам просто нужно рассмотреть правило eta другого конструктора типов, например, + вместо ->.

Это правило для двоичных сумм:

(case e of Lft y -> f (Lft y) | Rgt y -> f (Rgt y))  =  f e    (eta-+)

Это уравнение выполняется при энергичной оценке, поскольку e всегда будет уменьшаться с обеих сторон. При ленивой оценке, однако, г.ч.с. e уменьшает только если f также форсирует его. Это может сделать l.h.s. расходятся, где р.ч.с. не будет. Таким образом, уравнение не выполняется на ленивом языке.

Чтобы сделать это конкретным в Хаскеле:

f x = 0
lhs = case undefined of Left y -> f (Left y); Right y -> f (Right y)
rhs = f undefined

Здесь попытка печати lhs будет расходиться, тогда как rhs приведет к 0.

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

Основная проблема заключается в том, что при ленивом режиме каждый тип населяется _|_ (не прекращение), тогда как при нетерпении это не так. Это имеет серьезные семантические последствия. В частности, в Haskell нет индуктивных типов, и вы не можете доказать завершение структурной рекурсивной функции, например, обхода списка.

Существует ряд исследований в области теории типов, различающих типы данных (строгие) от типов кодированных данных (не строгие) и обеспечивающих оба способа двойным образом, что дает лучшее из обоих миров.

Редактировать: Что касается вопроса, почему компилятор не должен расширять функции eta: это полностью сломало бы каждый язык. На строгом языке с эффектами это наиболее очевидно, потому что возможность ставить эффекты через множественные абстракции функций - это особенность. Простейший пример, возможно, таков:

let make_counter () =
  let x = ref 0 in
  fun () -> x := !x + 1; !x

let tick = make_counter ()
let n1 = tick ()
let n2 = tick ()
let n3 = tick ()

Но эффекты - не единственная причина. Eta-расширение также может кардинально изменить производительность программы! Точно так же, как вы иногда хотите ставить эффекты, вы иногда также хотите ставить работа :

match :: String -> String -> Bool
match regex = \s -> run fsm s
  where fsm = ...expensive transformation of regex...

matchFloat = match "[0-9]+(\.[0-9]*)?((e|E)(+|-)?[0-9]+)?"

Обратите внимание, что я использовал Haskell здесь, потому что этот пример показывает, что неявное eta-расширение нежелательно ни в нетерпеливых, ни в ленивых языках!