HVM How?

全てのオブジェクトは1箇所にしか存在しないので Global な GC を必要としない
- Rust のように
- 複数参照がある場合, borrow system の代わりに lazy clone primitive を使う
  - on demand に clone する, データでなくラムダでも動作する
GHC よりも高速なのはラムダ内の計算の共有が可能なため
- from Lamping’s Abstract Algorithm for optimal evaluation of λ-calculus terms.
オブジェクトが1箇所にしか存在しないので並列化も単純に, atomic を1回しか使わない
この理論は前から知られていたが, 実装は項をグラフとして表現していた
- ポインタ参照が増えて遅い, SIC に基づくフォーマットで x50 faster
HVMは関数型プログラミング言語の最適評価に関する文献に由来している.
- The Optimal Implementation of Functional Programming Languages (Cambridge Tracts in Theoretical Computer Science, Series Number 45) のpp.14-39 を実用的に効率的に実装したものに過ぎない

syntax

term ::=
  | λvar. term               # a lambda
  | (term term)              # an application
  | (ctr term term ...)      # a constructor
  | num                      # a machine int
  | (op2 term term)          # an operator
  | let var = term; term     # a local definition

rule ::=
  | term = term

file ::= list<rule>

preliminary

λ は @ とかく
(Nil) == Nil
(((f a) b) c) == (f a b c)

clones ruin everything

function foo(x, y) {
	return x + x;
}

foo(2 * 2, 3 * 3) のとき

3 * 3 は無駄な計算
2 * 2 は2回計算される

かといってクローンを無くせば実用性が無くなる.

参照を使う

Haskell はlazy, 共有式への参照をメモしただけの thunk を作成し, 計算結果をキャッシュしたがλがあると破綻する(?)

thunk が自由変数を持つ計算を共有できない => λ内の式は全て無理
Rust は常に1つのオーナーしか許さず, コンパイラが安全と判断した場合にのみ参照を許す. 並列プログラミングは複雑

HVM’s solution: make clones deep

HVMはより広範なcloneを導入した.
: HVM runtimeには参照は無く, クローンされた値を読み込む必要があるまでゼロコストの .clone() を備えている.
読まれると, 全体がコピーされるのではなく, レイヤーごと(?) にon demand でコピーされる.

値がスコープから出たときにメモリ開放が出来る, 同じ理由で並列処理もほとんどスレッドセーフ
λをincremental にclone するには?

HVM’s Rewrite Rules

要するに Term Rewriting System
ユーザー定義ルールとプリミティブルールがある

User-defined Rules

(Foo (Tic a) (Tac b)) = (+ a b)

とファイルに書いたら

(Foo (Tic a) (Tac b))
--------------------- Foo-Rule-0
(+ a b)

としてくれる

Operations

(<op> x y)
------------------- Op2-U32
x +  y if <op> is +
x -  y if <op> is -
x *  y if <op> is *
x /  y if <op> is /
x %  y if <op> is %
x &  y if <op> is &
x |  y if <op> is |
x ^  y if <op> is ^
x >> y if <op> is >>
x << y if <op> is <<
x <  y if <op> is <
x <= y if <op> is <=
x == y if <op> is ==
x >= y if <op> is >=
x >  y if <op> is >
x != y if <op> is !=

定数演算

Number Duplication

dup x y = N
-----------
x <- N
y <- N

Constructor Duplication

dup x y = (Foo a b ...)
----------------------- Dup-Ctr
dup a0 a1 = a
dup b0 b1 = b
...
x <- (Foo a0 b0 ...)
y <- (Foo a1 b1 ...)

内部ではノード複製している. 言語に直接書くわけにはいかないのでコンパイラによって挿入される.
ex. (Foo a) = (+ a a) は (Foo a) = dup x y = a; (+ x y) になる
これにより全ての変数は1回だけ出現する.

Example

[1 + 1, 2 + 2, 3 + 3] のdup

dup x y = (Cons (+ 1 1) (Cons (+ 2 2) (Cons (+ 3 3) Nil)))
(Pair x y)
------------------------------------------- Dup-Ctr
dup x y = (Cons (+ 2 2) (Cons (+ 3 3) Nil))
dup a b = (+ 1 1)
(Pair
  (Cons a x)
  (Cons b y)
)
------------------------------------------- Op2-U32
dup x y = (Cons (+ 2 2) (Cons (+ 3 3) Nil))
dup a b = 2
(Pair
  (Cons a x)
  (Cons b y)
)
------------------------------------------- Dup-U32
dup x y = (Cons (+ 2 2) (Cons (+ 3 3) Nil))
(Pair
  (Cons 2 x)
  (Cons 2 y)
)
------------------------------------------- Dup-Ctr
dup x y = (Cons (+ 3 3) Nil)
dup a b = (+ 2 2)
(Pair
  (Cons 2 (Cons a x))
  (Cons 2 (Cons b y))
)
------------------------------------------- Op2-U32
dup x y = (Cons (+ 3 3) Nil)
dup a b = 4
(Pair
  (Cons 2 (Cons a x))
  (Cons 2 (Cons b y))
)
------------------------------------------- Dup-U32
dup x y = (Cons (+ 3 3) Nil)
(Pair
  (Cons 2 (Cons 4 x))
  (Cons 2 (Cons 4 y))
)
------------------------------------------- Dup-Ctr
dup x y = Nil
dup a b = (+ 3 3)
(Pair
  (Cons 2 (Cons 4 (Cons a x)))
  (Cons 2 (Cons 4 (Cons b y)))
)
------------------------------------------- Op2-U32
dup x y = Nil
dup a b = 6
(Pair
  (Cons 2 (Cons 4 (Cons a x)))
  (Cons 2 (Cons 4 (Cons b y)))
)
------------------------------------------- Dup-U32
dup x y = Nil
(Pair
  (Cons 2 (Cons 4 (Cons 6 x)))
  (Cons 2 (Cons 4 (Cons 6 y)))
)
------------------------------------------- Dup-Ctr
(Pair
  (Cons 2 (Cons 4 (Cons 6 Nil)))
  (Cons 2 (Cons 4 (Cons 6 Nil)))
)

(+ 1 1) がcloneされるわけではないことに注意
リストの一部しか使わないなら完全に複製する必要はない

Lambda Application

(λx(body) arg)
-------------- App-Lam
x <- arg
body

A modern CPU can perform more than 200 million beta-reductions per second

ex.

(λxλy(Pair x y) 2 3)
-------------------- App-Lam
(λy(Pair 2 y) 3)
-------------------- App-Lam
(Pair 2 3)

Haskell の thunk はこれをしている

Lambda Duplication

dup a b = λx(body)
------------------ Dup-Lam
a <- λx0(b0)
b <- λx1(b1)
x <- {x0 x1}
dup b0 b1 = body

dup a b = {r s}
--------------- Dup-Sup
a <- r
b <- s

λを複製するとλ内のvarとbodyも複製される.

Example.

dup a b = λx λy (Pair x y)
(Pair a b)

λ全体をコピーせずにincrementalにコピーする方法
一番外側のλをコピーすると

dup a b = λy (Pair x y)
(Pair λx(a) λx(b))

参照を持たなくなりだめ

ラムダにはスコープが無く, ラムダの外に出現する事ができる.
ex. (Pair x(λx(8) 7)) は(Pair 7 8) になる(?)

とすると, 2行目の λx の変数は1行目の x と繋がっている
-> 同じ変数に2つ束縛されている

そこで重ね合わせ(superposition) が必要.
ex. (Pair {1 2} 3) と書くと (Pair 1 3) と (Pair 2 3) が文脈によって変わる

dup a b = λx(λy(Pair x y))
(Pair a b)
------------------------------------------------ Dup-Lam
dup a b = λy(Pair {x0 x1} y)
(Pair λx0(a) λx1(b))
------------------------------------------------ Dup-Lam
dup a b = (Pair {x0 x1} {y0 y1})
(Pair λx0(λy0(a)) λx1(λy1(b)))
------------------------------------------------ Dup-Ctr
dup a b = {x0 x1}
dup c d = {y0 y1}
(Pair λx0(λy0(Pair a c)) λx1(λy1(Pair b d)))
------------------------------------------------ Dup-Sup
dup c d = {y0 y1}
(Pair λx0(λy0(Pair x0 c)) λx1(λy1(Pair x1 d)))
------------------------------------------------ Dup-Sup
(Pair λx0(λy0(Pair x0 y0)) λx1(λy1(Pair x1 y1)))

これでλ内部の計算を共有することが出来る. 例,

dup f g = ((λx λy (Pair (+ x x) y)) 2)
(Pair (f 10) (g 20))
-------------------------------------- App-Lam
dup f g = λy (Pair (+ 2 2) y)
(Pair (f 10) (g 20))
-------------------------------------- Dup-Lam
dup f g = (Pair (+ 2 2) {y0 y1})
(Pair (λy0(f) 10) (λy1(g) 20))
-------------------------------------- App-Lam
dup f g = (Pair (+ 2 2) {10 y1})
(Pair f (λy1(g) 20))
-------------------------------------- App-Lam
dup f g = (Pair (+ 2 2) {10 20})
(Pair f g)
-------------------------------------- Dup-Ctr
dup a b = (+ 2 2)
dup c d = {10 20}
(Pair (Pair a c) (Pair b d))
-------------------------------------- Op2-U32
dup a b = 4
dup c d = {10 20}
(Pair (Pair a c) (Pair b d))
-------------------------------------- Dup-U32
dup c d = {10 20}
(Pair (Pair 4 c) (Pair 4 d))
-------------------------------------- Dup-Sup
(Pair (Pair 4 10) (Pair 4 20))

(+ 2 2) が一度しか現れていない.

Superposed Application

({λx(x) λy(y)} 10) は dupする

({a b} c)
--------------- App-Sup
dup x0 x1 = c
{(a x0) (b x1)}

重ね合わせが含まれている時は dup して重ね合わせる

Superposed Duplication

dup x y = {a b}
--------------- Dup-Sup (different)
x <- {xA xB}
y <- {yA yB}
dup xA yA = a
dup xB yB = b

重ね合わせのdupはそれぞれのdupの重ね合わせ
これはλ applicationで既に出てきてルールが衝突するので制限をつける.

argをcloneするλ自身がcloneされるときに, そのクローン同士がクローンし合うのはng

ex.

let g = λf(λx(f (f x)))
(g g)

チャーチ符号化された自然数でループとかしなければ恐らくこの形にならない.

Quartz 5

Explorer

HVM HOW