为什么GHC让修复变得如此混乱？ [英] Why does GHC make fix so confounding?

问题描述

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

  fix ::（a  - > a） - > a 
修复f = let x = fx in x 
  

在一个示例修复

使用像这样：

  fix（\fx  - > let x'= x + 1 in x ：f x'）
  

这基本上会产生一个数字序列，从1增加到无穷大。发生这种情况修复必须将其收到的功能作为第一个参数来修改它。我不清楚上面列出的 fix 的定义是如何做到的。

这个定义是我如何理解修复工程：

 修复::（a  - > a） - > a 
修复f = f（修复f）
  

现在我有两个问题：

1. x 在第一个定义中是如何表示修复x 的？


2. 对第二个定义使用第二个定义有什么好处？
   

解决方案

 修复::（a  - >> / div> 
使用等式推理很容易看出这个定义是如何工作的。 ; a） - > a 
修正f = let x = fx in x 
  

x 评估当我们尝试评估修复f ？它定义为 f x ，所以修复f = f x 。但是这里 x 是什么？它与以前一样 f x 。所以你得到修复f = f x = f（f x）。以这种方式进行推理可以得到一个无限的 f 应用程序链：修复f = f （f（f ...）））。

现在，将（\fx - > ;让x'= x + 1 in x：f x'） for f 您会得到

  fix（\ fx  - > let x'= x + 1 in x：f x'）
 =（\ fx  - > 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）= x + 1 in x：（f ...）x'）x + 1））
 =（\ x  - > x：（（\ x  - > x： 。）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 = __整数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字节
在GC 
期间复制的133,012字节最大居民地址（1个样本）27,040字节
 17,688字节最大地址
 1 MB总内存使用量（由于碎片造成0 MB丢失）
 [...] 
  

将它与行为进行比较第一个程序：

  $ ./Test1 + RTS -s 
分配给堆的47,168字节
 1,756在GC 
期间复制的字节数最大居民身份（1个样本）
 18,808字节最大值slb 
使用的总内存量（由于分段而丢失的0 MB）
 [ ...] 
  

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

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. How does x ever come to mean fix x in the first definition?
2. Is there any advantage to using the first definition over the second?

解决方案

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

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 ...))).

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))
    = ...

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

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

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:

Now let's look at 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

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让修复变得如此混乱？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！