Почему GHC делает исправление настолько запутанным?

Ответ 1

Легко понять, как это определение работает, применяя эквациональные рассуждения.

fix :: (a -> a) -> a
fix f = let x = f x in x

Что будет оценивать x при попытке оценить fix f? Он определяется как f x, поэтому fix f = f x. Но что здесь x? Это f x, как и раньше. Итак, вы получите fix f = f x = f (f x). Рассуждая таким образом, вы получаете бесконечную цепочку приложений f: fix f= f (f (f (f ...))).

Теперь, заменив (\f x -> let x' = x+1 in x:f x') на f, вы получите

fix (\f x -> let x' = x+1 in x:f x')
    = (\f x -> let x' = x+1 in x:f x') (f ...)
    = (\x -> let x' = x+1 in x:((f ...) x'))
    = (\x -> x:((f ...) x + 1))
    = (\x -> x:((\x -> let x' = x+1 in x:(f ...) x') x + 1))
    = (\x -> x:((\x -> x:(f ...) x + 1) x + 1))
    = (\x -> x:(x + 1):((f ...) x + 1))
    = ...

Изменить. Что касается вашего второго вопроса, @is7s указал в комментариях, что первое определение предпочтительнее, потому что оно более эффективно.

Чтобы узнать, почему, давайте посмотрим на Core для fix1 (:1) !! 10^8:

a_r1Ko :: Type.Integer    
a_r1Ko = __integer 1

main_x :: [Type.Integer]   
main_x =
  : @ Type.Integer a_r1Ko main_x

main3 :: Type.Integer
main3 =
  !!_sub @ Type.Integer main_x 100000000

Как вы можете видеть, после преобразований fix1 (1:) по существу стало main_x = 1 : main_x. Обратите внимание, как это определение относится к самому себе - вот что означает "связывание узла". Эта самореклама представляется как простая указательная ссылка во время выполнения:

Теперь посмотрим на fix2 (1:) !! 100000000:

main6 :: Type.Integer
main6 = __integer 1

main5
  :: [Type.Integer] -> [Type.Integer]
main5 = : @ Type.Integer main6

main4 :: [Type.Integer]
main4 = fix2 @ [Type.Integer] main5

main3 :: Type.Integer
main3 =
  !!_sub @ Type.Integer main4 100000000

Здесь приложение fix2 фактически сохраняется:

В результате вторая программа должна выполнять распределение для каждого элемента списка (но поскольку список сразу же потребляется, программа по-прежнему эффективно работает в постоянном пространстве):

$ ./Test2 +RTS -s
   2,400,047,200 bytes allocated in the heap
         133,012 bytes copied during GC
          27,040 bytes maximum residency (1 sample(s))
          17,688 bytes maximum slop
               1 MB total memory in use (0 MB lost due to fragmentation)
 [...]

Сравните это с поведением первой программы:

$ ./Test1 +RTS -s          
          47,168 bytes allocated in the heap
           1,756 bytes copied during GC
          42,632 bytes maximum residency (1 sample(s))
          18,808 bytes maximum slop
               1 MB total memory in use (0 MB lost due to fragmentation)
[...]

Ответ 2

Как x когда-либо понимается как fix x в первом определении?

fix f = let x = f x in x

Пусть привязки в Haskell рекурсивные

Прежде всего, поймите, что Haskell позволяет рекурсивно связывать привязки. Что Haskell называет "let", некоторые другие языки называют "letrec". Это нормально для определения функций. Например:

ghci> let fac n = if n == 0 then 1 else n * fac (n - 1) in fac 5
120

Но это может показаться странным для определения значений. Тем не менее, значения могут быть рекурсивно определены из-за неустойчивости Haskell.

ghci> take 5 (let ones = 1 : ones in ones)
[1,1,1,1,1]

См. Нежное введение в Haskell в разделах 3.3 и 3.4 для более подробной информации о ленивости Haskell.

Thunks в GHC

В GHC пока еще не оцененное выражение завернуто в "thunk": обещание выполнить вычисление. Тонки оцениваются только тогда, когда они абсолютно необходимы. Предположим, что мы хотим fix someFunction. Согласно определению fix, это

let x = someFunction x in x

Теперь, что видит GHC, это что-то вроде этого.

let x = MAKE A THUNK in x

Таким образом, он счастливо делает для вас удар и движется прямо до тех пор, пока вы не спросите, что на самом деле x.

Оценка образца

Это выражение thunk просто имеет отношение к самому себе. Возьмем пример ones и перепишем его для использования fix.

ghci> take 5 (let ones recur = 1 : recur in fix ones)
[1,1,1,1,1]

Итак, как будет выглядеть этот трюк?
Мы можем встроить ones в качестве анонимной функции \recur -> 1 : recur для более четкой демонстрации.

take 5 (fix (\recur -> 1 : recur))

-- expand definition of fix
take 5 (let x = (\recur -> 1 : recur) x in x)

Итак, что такое x? Ну, хотя мы не совсем уверены в том, что x, мы все равно можем воспользоваться приложением функции:

take 5 (let x = 1 : x in x)

Эй, посмотрим, мы вернулись к определению, которое у нас было раньше.

take 5 (let ones = 1 : ones in ones)

Итак, если вы считаете, что понимаете, как это работает, тогда вы хорошо чувствуете, как работает fix.

Есть ли какое-либо преимущество в использовании первого определения над вторым?

Да. Проблема в том, что вторая версия может вызвать утечку пространства даже при оптимизации. См. билет GHC traС# 5205, для аналогичной проблемы с определением forever. Вот почему я упомянул thunks: потому что let x = f x in x выделяет только один thunk: x thunk.

Ответ 3

Разница заключается в совместном использовании и копировании. ¹

fix1 f = x where x = f x    -- more visually apparent way to write the same thing

fix2 f = f (fix2 f)

Если мы подставим определение в себя, то оба будут уменьшены как одна и та же бесконечная цепочка приложений f (f (f (f (f ...)))). Но первое определение использует явное именование; в Haskell (как и в большинстве других языков) совместное использование разрешено возможностью назвать вещи: одно имя более или менее гарантировано относится к одному "сущности" (здесь x). Второе определение не гарантирует совместного использования - результат вызова fix2 f заменяется на выражение, поэтому его можно также заменить на значение.

Но данный компилятор теоретически может быть умным и использовать совместное использование во втором случае.

Связанная проблема: " Y комбинатор". В нетипизированном лямбда-исчислении, где нет конструкций именования (и, следовательно, нет самореференции), комбинатор Y эмулирует самооценку, организуя определение, которое нужно скопировать, поэтому обращение к копии self становится возможным, Но в реализациях, которые используют модель среды для обозначения названных объектов на языке, становится возможной прямая ссылка по имени.

Чтобы увидеть более резкое различие между двумя определениями, сравните

fibs1 = fix1 ( (0:) . (1:) . g ) where g (a:[email protected](b:_)) = (a+b):g t
fibs2 = fix2 ( (0:) . (1:) . g ) where g (a:[email protected](b:_)) = (a+b):g t

См. также:

• В схеме, как вы используете лямбда для создания рекурсивной функции?
• Y combinator обсуждение в разделе "Маленькая схема"
• Можно ли использовать для создания бесконечных списков?

(особенно попытайтесь выработать последние два определения в предыдущей ссылке выше).

¹ Используя определения, для вашего примера fix (\g x -> let x2 = x+1 in x : g x2) получаем

fix1 (\g x -> let x2 = x+1 in x : g x2)
 = fix1 (\g x -> x : g (x+1))
 = fix1 f where {f = \g x -> x : g (x+1)}
 = fix1 f where {f g x = x : g (x+1)}
 = x      where {x = f x ; f g x = x : g (x+1)}
 = g      where {g = f g ; f g x = x : g (x+1)}   -- both g in {g = f g} are the same g
 = g      where {g = \x -> x : g (x+1)}           -- and so, here as well
 = g      where {g x = x : g (x+1)}

и, таким образом, собственно рекурсивное определение для g фактически создано. (в приведенном выше случае мы пишем ....x.... where {x = ...} для let {x = ...} in ....x...., для удобочитаемости).

Но второй вывод происходит с критическим различием подстановки значения назад, а не имени, как

fix2 (\g x -> x : g (x+1))
 = fix2 f             where {f g x = x : g (x+1)}
 = f (fix2 f)         where {f g x = x : g (x+1)}
 = (\x-> x : g (x+1)) where {g = fix2 f ; f g x = x : g (x+1)}
 = h                  where {h   x = x : g (x+1) ; g = fix2 f   ; f g x = x : g (x+1)}

чтобы фактический вызов продолжался, например,

take 3 $ fix2 (\g x -> x : g (x+1)) 10
 = take 3 (h 10)      where {h   x = x : g (x+1) ; g = fix2 f   ; f g x = x : g (x+1)}
 = take 3 (x:g (x+1)) where {x = 10 ;              g = fix2 f   ; f g x = x : g (x+1)}
 = x:take 2 (g x2)    where {x2 = x+1 ; x = 10 ;   g = fix2 f   ; f g x = x : g (x+1)}
 = x:take 2 (g x2)    where {x2 = x+1 ; x = 10 ; g = f (fix2 f) ; f g x = x : g (x+1)}
 = x:take 2 (x2 : g2 (x2+1))   where {             g2 = fix2 f  ;
                             x2 = x+1 ; x = 10 ;                  f g x = x : g (x+1)}
 = ......

и мы видим, что здесь устанавливается новая привязка (для g2) вместо предыдущей (для g), которая используется повторно как определение fix1.

Ответ 4

У меня есть, возможно, немного упрощенное объяснение, которое исходит из inlining оптимизации. Если мы имеем

fix :: (a -> a) -> a
fix f = f (fix f)

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

Однако

fix' f = let x = f x in x

не является рекурсивной функцией - она ​​никогда не называет себя. Только x внутри является рекурсивным. Поэтому при вызове

fix' (\r x -> let x' = x+1 in x:r x')

компилятор может встроить его в

(\f -> (let y = f y in y)) (\r x -> let x' = x+1 in x:r x')

а затем продолжить его упрощение, например

let y = (\r x -> let x' = x+1 in x:r x') y in y 
let y = (\  x -> let x' = x+1 in x:y x')   in y 

как будто функция была определена с использованием стандартного рекурсивного обозначения без fix:

    y       x =  let x' = x+1 in x:y x'