为什么GHC让修复如此混乱?

Van*_*uel 15 recursion haskell fixpoint-combinators

看一下GHC源代码,我可以看到修复的定义是:

fix :: (a -> a) -> a
fix f = let x = f x in x
Run Code Online (Sandbox Code Playgroud)

在一个示例中,修复程序使用如下:

fix (\f x -> let x' = x+1 in x:f x')
Run Code Online (Sandbox Code Playgroud)

这基本上产生了一个数字序列,它们增加1到无穷大.为了实现这一点,修复必须将它接收的函数作为它的第一个参数直接回到该函数.我不清楚上面列出的修复定义是如何做到的.

这个定义是我如何理解修复的工作原理:

fix :: (a -> a) -> a
fix f = f (fix f)
Run Code Online (Sandbox Code Playgroud)

所以现在我有两个问题:

  1. 如何X真的来临意味着修复X中的第一个定义?
  2. 在第二个定义中使用第一个定义是否有任何优势?

Mik*_*kov 16

通过应用等式推理,很容易看出这个定义是如何工作的.

fix :: (a -> a) -> a
fix f = let x = f x in x
Run Code Online (Sandbox Code Playgroud)

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))
    = ...
Run Code Online (Sandbox Code Playgroud)

编辑:关于你的第二个问题,@ 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
Run Code Online (Sandbox Code Playgroud)

正如您所看到的,在转换fix1 (1:)基本上成为了main_x = 1 : main_x.请注意这个定义如何引用自身 - 这就是"打结"的意思.这个自引用在运行时表示为一个简单的指针间接:

fix1

现在让我们来看看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
Run Code Online (Sandbox Code Playgroud)

这里fix2应用程序实际上是保留的:

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)
 [...]
Run Code Online (Sandbox Code Playgroud)

将其与第一个程序的行为进行比较:

$ ./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)
[...]
Run Code Online (Sandbox Code Playgroud)

  • 第一个定义更有效,因为它结合了一个结.例如,比较`fix1(1 :) !! 1000000`和`fix2(1 :) !! 1000000`. (9认同)
  • @MikhailGlushenkov不,`-O2`的第一个定义仍然快得多.尝试使用更大的数字,如"100000000".它在我的机器上快了约5倍. (3认同)

Dan*_*ton 9

x如何在第一个定义中修复x?

fix f = let x = f x in x
Run Code Online (Sandbox Code Playgroud)

让Haskell中的绑定是递归的

首先,要意识到Haskell允许递归let绑定.Haskell称之为"let",其他一些语言称之为"letrec".对于函数定义,这感觉很正常.例如:

ghci> let fac n = if n == 0 then 1 else n * fac (n - 1) in fac 5
120
Run Code Online (Sandbox Code Playgroud)

但是对于价值定义来说,这似乎很奇怪.然而,由于Haskell的非严格性,可以递归地定义值.

ghci> take 5 (let ones = 1 : ones in ones)
[1,1,1,1,1]
Run Code Online (Sandbox Code Playgroud)

有关Haskell懒惰的详细说明,请参阅Haskell第3.3和3.4节的简要介绍.

在GHC中的thunk

在GHC中,一个尚未评估的表达式被包含在"thunk"中:承诺执行计算.只有绝对必须的时候才会评估Thunks .假设我们想要fix someFunction.根据定义fix,那是

let x = someFunction x in x
Run Code Online (Sandbox Code Playgroud)

现在,GHC看到的是这样的.

let x = MAKE A THUNK in x
Run Code Online (Sandbox Code Playgroud)

所以它很乐意为你做一个thunk,并一直向前移动,直到你要求知道x实际是什么.

样品评估

那个thunk的表达恰好是指自己.让我们ones举个例子并重写它来使用fix.

ghci> take 5 (let ones recur = 1 : recur in fix ones)
[1,1,1,1,1]
Run Code Online (Sandbox Code Playgroud)

那个thunk会是什么样子?
我们可以将内联ones作为匿名函数\recur -> 1 : recur进行更清晰的演示.

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

-- expand definition of fix
take 5 (let x = (\recur -> 1 : recur) x in x)
Run Code Online (Sandbox Code Playgroud)

那么,那 x什么?好吧,即使我们不确定是什么x,我们仍然可以使用函数应用程序:

take 5 (let x = 1 : x in x)
Run Code Online (Sandbox Code Playgroud)

嘿看,我们回到了以前的定义.

take 5 (let ones = 1 : ones in ones)
Run Code Online (Sandbox Code Playgroud)

所以,如果你相信你理解那个是如何运作的,那么你就会很好地理解是如何fix运作的.


在第二个定义中使用第一个定义是否有任何优势?

是.问题是第二个版本可能导致空间泄漏,即使有优化.有关定义的类似问题,请参阅GHC trac ticket#5205forever.这就是我提到thunks的原因:因为let x = f x in x只分配了一个thunk:xthunk.


Wil*_*ess 5

区别在于共享与复制.1

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

fix2 f = f (fix2 f)
Run Code Online (Sandbox Code Playgroud)

如果我们将定义替换为自身,则两者都被缩减为相同的无限应用链 f (f (f (f (f ...)))).但第一个定义使用显式命名; 在Haskell中(与大多数其他语言一样)共享是通过命名事物的能力来实现的:一个名称或多或少地保证引用一个"实体"(这里x).第二个定义不保证任何共享 - 调用的结果fix2 f被替换为表达式,因此它也可以替换为值.

但是理论上给定的编译器在理论上可以很聪明,并且在第二种情况下也可以使用共享.

相关问题是" Y组合者".在无类型的lambda演算中,没有命名结构(因此没有引用),Y组合器通过安排要复制的定义来模拟自引用,因此引用自我的副本变得可能.但是在使用环境模型来允许语言中的命名实体的实现中,可以通过名称直接引用.

要比较两个定义之间的更大差异,请进行比较

fibs1 = fix1 ( (0:) . (1:) . g ) where g (a:t@(b:_)) = (a+b):g t
fibs2 = fix2 ( (0:) . (1:) . g ) where g (a:t@(b:_)) = (a+b):g t
Run Code Online (Sandbox Code Playgroud)

也可以看看:

(特别是尝试在上面的最后一个链接中计算出最后两个定义).


1根据定义,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)}
Run Code Online (Sandbox Code Playgroud)

因此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)}
Run Code Online (Sandbox Code Playgroud)

所以实际的呼叫将继续进行,例如

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)}
 = ......
Run Code Online (Sandbox Code Playgroud)

我们看到在这里建立了一个新的绑定(for g2),而不是gfix1定义那样重用前一个(for ).


Pet*_*lák 5

我可能有一些简化的解释来自内联优化.如果我们有

fix :: (a -> a) -> a
fix f = f (fix f)
Run Code Online (Sandbox Code Playgroud)

那么它fix是一个递归函数,这意味着它不能在使用它的地方内联(INLINE如果给定,pragma将被忽略).

然而

fix' f = let x = f x in x
Run Code Online (Sandbox Code Playgroud)

不是一个递归函数-它永远不会调用自身.只有x里面是递归的.所以在打电话时

fix' (\r x -> let x' = x+1 in x:r x')
Run Code Online (Sandbox Code Playgroud)

编译器可以将其内联到

(\f -> (let y = f y in y)) (\r x -> let x' = x+1 in x:r x')
Run Code Online (Sandbox Code Playgroud)

然后继续简化它,例如

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 
Run Code Online (Sandbox Code Playgroud)

这就好像函数是使用标准递归表示法定义的,没有fix:

    y       x =  let x' = x+1 in x:y x'   
Run Code Online (Sandbox Code Playgroud)