为什么 GHC 使修复如此令人困惑?

问题描述

查看 GHC 源代码我可以看到 fix 的定义是:

Looking at the GHC source code I can see that the definition for fix is:

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

在一个例子中 fix 是这样使用的:

In an example fix is used like this:

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

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

This basically yields a sequence of numbers that increase by one to infinity. For this to happen fix must be currying the function that it receives right back to that very function as it's first parameter. It isn't clear to me how the definition of fix listed above could be doing that.

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

This definition is how I came to understand how fix works:

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

所以现在我有两个问题:

So now I have two questions:

1. 在第一个定义中 x 是如何表示 fix x 的?
2. 使用第一个定义比使用第二个有什么优势吗?

推荐答案

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

It's easy to see how this definition works by applying equational reasoning.

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

当我们尝试对 fix f 求值时，x 会求什么值?它被定义为f x，所以fix f = f x.但是这里的 x 是什么?和以前一样，它是 f x.所以你得到 fix f = f x = f (f x).以这种方式推理你会得到f的无限应用链:fix f = f (f (f (f ...))).

What will x evaluate to when we try to evaluate fix f? It's defined as f x, so fix f = f x. But what is x here? It's f x, just as before. So you get fix f = f x = f (f x). Reasoning in this way you get an infinite chain of applications of f: fix f = f (f (f (f ...))).

现在，用 (f x -> let x' = x+1 in x:f x') 替换 f 你得到

Now, substituting (f x -> let x' = x+1 in x:f x') for f you get

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 在评论中指出第一个定义更可取，因为它更有效.

Edit: Regarding your second question, @is7s pointed out in the comments that the first definition is preferable because it is more efficient.

要找出原因，让我们看看 fix1 (:1) 的核心！10^8:

To find out why, let's look at the Core for 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.注意这个定义是如何指代自身的——这就是打结"的意思.这个自引用在运行时表示为一个简单的指针间接:

As you can see, after the transformations fix1 (1:) essentially became main_x = 1 : main_x. Note how this definition refers to itself - this is what "tying the knot" means. This self-reference is represented as a simple pointer indirection at runtime:

现在让我们看看 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 应用程序:

Here the fix2 application is actually preserved:

结果是第二个程序需要为链表的每个元素做分配(但由于链表立即被消耗掉，程序仍然有效地运行在恒定空间中):

The result is that the second program needs to do allocation for each element of the list (but since the list is immediately consumed, the program still effectively runs in constant space):

$ ./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)
 [...]

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

Compare that to the behaviour of the first program:

$ ./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)
[...]

这篇关于为什么 GHC 使修复如此令人困惑?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！