9

ZINC以及partial apply

 3 years ago
source link: https://www.zenlife.tk/zinc.md
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

ZINC以及partial apply

2016-09-22

最早是带着疑惑:ML语言里面的partial apply是如何实现的?比如,scheme语言里面 (define (add x y) (+ x y)) 不允许 (add 3) ,在ML里面可以。

然后发现了这个slide,讲OCaml的实现是如何一步步演进成现在这样子的:

http://pauillac.inria.fr/~xleroy/talks/zam-kazam05.pdf

ML的抽象机模型用的不是scheme中常见的SECD,是一种叫ZINC的东西。这个slide读了好久,主要是越看不懂的越多,现在总算是懂了六七成吧,至少整个过程是从发散到收敛了。有时候就是这样,读一篇文章发现有些点不理解,再去搜相关的东西,又遇到了更多不理解的点,整个发散下去就变成读一个领域了,PL和编译器相关的都是巨坑!

de Bruijn index

先说de Bruijn index表示,跟scheme那边的不同是从de Bruijn index表示开始的。

λx. λy. x	=>	λ λ 1
λx. λy. λz. x z (y z)	=>	λ λ λ 2 0 (1 0)
λz. (λy. y (λx. x)) (λx. z x)	=>	λ (λ 1 (λ 1)) (λ 2 1)

de Bruijn index是lambda演算另一种表示形式,去掉了参数名的概念,直接用出现的位置来表示变量。比如说出现在本层的lambda绑定,就是0。λx. x 等价于 λ 0 ,上面的第一个例子 λx. λy. x 中,x出现在上一层的位置,所以是 λ λ 1 。类似的,如果出现在再上一层的lambda绑定就是2。free variable这里就不讲了,有兴趣自己去查查。

这种表示省掉了alpha变换,并且由于没有了name,环境的表示也就跟scheme不同了(其实也没什么本质的区别,可以看作一种是hash表由key-value查变量,另一种是由数组下标查变量)。

CAM(Categorical Abstract Machine)

CAM的编译很简单,规则就这几个:

C[n] = ACCESS(n)
C[λa] = CLOSURE(C[a]; RETURN)
C[a b] = C[a]; C[b]; APPLY
解释一下就是,变量直接编译成环境访问,由于是Bruijn index表示的,也就是直接变成在环境中的偏移。lambda的编译就生成闭包指令,apply的编译都很直观。

相应的指令:

ACCESS(n)	将环境的第n个对象进栈
CLOSURE(c)	由代码c和当前环境创建闭包,将闭包进栈
APPLY	调这条指令时,当前栈上的内容是参数和闭包,用闭包中的代码和环境替换掉虚拟机的代码和环境
RETURN	调这条指令时,栈上的是一个闭包(APPLY指令保存下来的),用它替换虚拟机的代码和环境
注意在APPLY的时候,当前上下文(代码&环境)替换为闭包中上下文的同时,是要将当前代码&环境保存并进栈,作为返回地址。除了使用的是Bruinj index表示,CAM跟SECD还是比较像的。

简单lambda演算都是用一个参数的。CAM的问题是做Currying会产生太多的临时闭包(SECD同理)。每多一个参数都产生闭包 fun x y z ... 要变成 λx. λy. λz 会生成三次闭包。

ZAM(ZINC Abstract Machine)

其实避免生成闭包并不困难,稍微改动一下。之前的CAM模型,以及没有做partial apply支持的SECD等,都是由调用者准备好所有的参数,然后调用。如果参数不够或者参数多了,就报错。修改后,不要由调用函数去检查参数。

由被调函数去判断是否有足够的参数,如果有就执行函数体,否则生成partial apply的闭包。

整个在之前的基础上添加了GRAB指令,就是在刚进入函数后执行,检查参数以决定执行函数体还是生成partial apply的闭包。这些变化就是从CAM进化到ZINC。

在此之前Krivine's Machine。Krivine' Machine的编译规则如下:

C[n] = ACCESS(n)
C[λa] = GRAB; C[a]
C[a b] = PUSH(C[b]); C[a]
相应的指令
ACCESS	用环境的第n个对象(闭包),替换掉当前代码和环境
PUSH	将PUSH指令里的代码跟当前环境形成闭包,闭包进栈
GRAB	将栈上的闭包出栈,进到环境
理解Krivine's Machine重要的两点:
  1. C[λa]的时候并不构建闭包,这跟CAM/SECD一类其它抽象机器都不同(效果是做currying没有任何额外负担)。
  2. delay求值的策略,在C[a b]的时候并不将b求值,而是变成闭包了。

为什么讲到Krivine's Machine呢?因为ZINC其实是一种Krivine's Machine变种。区别是标准的Krivine's Machine是call by name的,而ZINC是严格求值的call by value的变种。

ZINC的编译和指令有点长,这里就不写了,见之前slide里面的第14、15页。

接下来是再从ZINC到Caml Light,就只是一些优化了,包括合并调用栈和返回值栈,优化环境表示,编译期决定更多的东西。

说一下对于环境的表示的优化,用栈来表示环境,而不是堆,只有当真正需要生成闭包时,才会用到堆。

环境是一个支持下列操作的东西:

add(v1, . . . , vn, e)	将v1...vn加入到环境中
accessn(e)	返回环境中的第n个元素
close(c, e)	用环境生成一个闭包

至于环境用栈表示或用堆表示,并不需要关心。于是优化可以做成平时在栈上,只有当需要生成闭包时,把栈上的数据拷到堆上,生成闭包。


About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK