歡迎移駕該處參與討論 :)
此篇的內容主要整理自 Deriving Compilers and Virtual Machines for a Multi-Level Language 一文
( http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/papers/VMcircle.html )，
不過稍微多加上一點東西。算是讀後練習分享吧。
本篇文章意圖從一個簡單的Multi-level language specification推導出一個compiler和一個較有效率的Virtual Machine。
Multi-Stage Programming讓我們可以寫出generic和highly-parameterized program，
但是卻不需要付出不必要的runtime overheads。
( 更多MSP的資訊可以參考這裡: http://www.cs.rice.edu/~taha/MSP/ )
一開始我們有一個簡單的Multi-level Language。
data Term = Lit Int | Var Int | Add Term Term | Abs Term | App Term Term
| Next Term | Prev Term
data Val = Clos Term Env | Quot Term | Val Int
type Env = [Val]
type Cont = Val -> Val
Terms包含了Integer, Variable, Addition, Lambda-abstraction, Application，
最後還有兩個Level-Operator。
我們用de Bruijn index來表示variable，所以Var後面是Int。
一個Value是一個closure,一個quoted term或是某一個value n。
而Environment是一個list of value。
最後，為了要清楚的表示整個control flow和data flow，
我們用CPS(Continuation Passing Style)來寫evaluator。
而為了讓Continuation比較好看懂，我們再宣告Cont是一個value to value 的function。
以上，有幾個地方要稍微多注意一下。
首先，因為我們用de Bruijn index來表示variables。
每當λ○-term中出現一個level n(n ≠ 0)的λ-binder時，
我們會需要把Environment中所有level n的variables都+1，
以避免未來產生variable capture的問題。
因此我們需要一個shiftE的function來幫我們修改整個Environment。
而我們實際要改的是每一個variable也就是term，
所以我們也還要一個shift來改term。
shiftE :: Int -> Env -> Env
shiftE _ [] = []
shiftE l (x:xs) = case x of
(Clos t e) -> (Clos (shift 0 l t) e) : (shiftE l xs)
(Quot t) -> (Quot (shift 0 (l-1) t)) : (shiftE l xs)
(Val n) -> (Val n) : (shiftE l xs)
shift :: Int -> Int -> Term -> Term
shift j l (Var n) = case (n >= j) && (l == 0) of
True -> Var (n+1)
False -> Var n
shift j l (Lit n) = Lit n
shift j l (Add t t') = Add (shift j l t) (shift j l t')
shift j l (Abs t) = Abs (shift (j+1) l t)
shift j l (App t0 t1) = App (shift j l t0) (shift j l t1)
shift j l (Next t) = Next (shift j (l-1) t)
shift j l (Prev t) = Prev (shift j (l+1) t)
接著是Next和Prev的問題。
如果先不管Next和Prev。
那麼剩下的部份我們可以當是一個簡單的lambda-calculus。
但是因為我們想要表示一些"現在先不要做的事情"，
所以我們從Linear-Time Temporal Logic裡面借個東西出來表示"某物是未來才要算的"。
這也就是我們的Next。(Next在Temporal Logic裡面寫成○)
此時，這裡的term就不再是簡單的λ-term，而是λ○-term。
我們寫出來的λ○-term可以說是一個"算到一半的程式"，
因為他裡面有包含到一些"未來再一次運算時才要計算"的資訊。
換句話說，如果是在partial evaluation裡面，
我們可以把λ○-term當作是Multi-Level Generating Extension。
這意思就是說，它可以一直去拿新的input然後產生出剩下的program(也就是另一個λ○-term)。
現在我們有了Next，我們可以用Next表示未來某個時間要算的東西。
但是我們還需要一個東西來處理"例外"的情況。
考慮一個情形，假設我們現在有Next t1 t2 t3 ...這樣的λ○-term。
這表示說我們在下一次evaluating時才真的需要去算那些t1, t2, ...。
可是假使現在其中一個 tn 是在現在這一個步驟就可以先算的，
那我們就需要另一個operator來讓 tn 脫離前面Next的魔掌。
而這個operator就是Prev。
來看簡單的例子
eval (Next (1 + 2)) => Quot (1+2)
eval (Next (Prev (1 + 2))) => Val 3
接著我們終於可以直接開始寫我們的evaluator。
我們的evaluator需要拿一個λ○-term, level, environment 和 continuation，
而最後會算出一個value。
這個evaluator做的事情很簡單。
如果拿到的term是level 0，就直接看他是什麼就算什麼。
是literal n那就回傳 value n，是 variable m那就去environment裡面找第m個，以此類推。
例外的只有Prev，因為Prev的base case是level 1，不是level 0。
而如果拿到的term是level n(n ≠ 0)，
那就把term的constructor外面包上一層Quot，然後往裡面繼續做。
例如說 eval (Abs t) le env k => Quot (Abs (eval t le env k))。
eval0 :: Term -> Int -> Env -> Cont -> Val
eval0 (Lit n) 0 e k = k (Val n)
eval0 (Var n) 0 e k = k (e!!n)
eval0 (Next t) 0 e k = eval0 t 1 e (/(Quot t') -> k (Quot t'))
eval0 (Prev t) 1 e k = eval0 t 0 e (/v -> case v of
(Quot t') -> k (Quot t')
(Val n) -> k (Quot (Lit n)))
eval0 (Abs t) 0 e k = k (Clos t e)
eval0 (App t1 t2) 0 e k = eval0 t1 0 e (/(Clos t1' e') ->
eval0 t2 0 e (/val ->
eval0 t1' 0 (val:e') k))
eval0 (Add t1 t2) 0 e k = eval0 t1 0 e (/(Val m) ->
eval0 t2 0 e (/(Val n) ->
k (Val (m + n))))
eval0 (Lit n) l e k = k (Quot (Lit n))
eval0 (Var n) l e k = k (Quot (Var n))
eval0 (Next t) l e k = eval0 t (l+1) e (/(Quot t) -> k (Quot (Next t)))
eval0 (Prev t) l e k = eval0 t (l-1) e (/(Quot t) -> k (Quot (Prev t)))
eval0 (Abs t) l e k = eval0 t l (shiftE l e) (/(Quot t) -> k (Quot (Abs t)))
eval0 (App t1 t2) l e k =
eval0 t1 l e (/(Quot t1') ->
eval0 t2 l e (/(Quot t2') ->
k (Quot (App t1' t2'))))
eval0 (Add t1 t2) l e k =
eval0 t1 l e (/(Quot t1') ->
eval0 t2 l e (/(Quot t2') ->
k (Quot (Add t1' t2'))))
有了上面evaluator的definition，就可以開始deriving了。
首先，第一步，我們嫌Continuation的部份都是lambda function不方便看。
所以我們針對continuation的部份做一次defunctionalze。
把Continuation的部份另外用一個first-order data來表示。
所以我們先把
type Cont = Val -> Val
改成
data Cont = Cont0 | Cont1 ... | ...
然後再去定義另一個function來處理這個Cont的部份。
eval1 :: Term -> Int -> Env -> Cont -> Val
eval1 (Lit n) 0 e k = appK1 k (Val n) -- Cont0
eval1 (Var n) 0 e k = appK1 k (e!!n) -- Cont0
eval1 (Abs t) 0 e k = appK1 k (Clos t e) -- Cont0
eval1 (Next t) 0 e k = eval1 t 1 e (Cont1 k) -- Cont1
eval1 (Prev t) 1 e k = eval1 t 0 e (Cont2 k) -- Cont2
eval1 (App t1 t2) 0 e k = eval1 t1 0 e (Cont3 t2 e k) -- Cont3 Cont4
eval1 (Add t1 t2) 0 e k = eval1 t1 0 e (Cont5 t2 e k) -- Cont5 Cont6
eval1 (Lit n) l e k = appK1 k (Quot (Lit n)) -- Cont0
eval1 (Var n) l e k = appK1 k (Quot (Var n)) -- Cont0
eval1 (Abs t) l e k = eval1 t l (shiftE l e) (Cont7 k) -- Cont7
eval1 (Next t) l e k = eval1 t (l+1) e (Cont8 k) -- Cont8
eval1 (Prev t) l e k = eval1 t (l-1) e (Cont9 k) -- Cont9
eval1 (App t1 t2) l e k = eval1 t1 l e (Cont10 t2 l e k) -- Cont10 Cont11
eval1 (Add t1 t2) l e k = eval1 t1 l e (Cont12 t2 l e k) -- Cont12 Cont13
appK1 :: Cont -> Val -> Val
appK1 (Cont0) val = val
appK1 (Cont1 ct) (Quot tm) = appK1 ct (Quot tm)
appK1 (Cont2 ct) (Quot tm) = appK1 ct (Quot tm)
appK1 (Cont2 ct) (Val n) = appK1 ct (Quot (Lit n))
appK1 (Cont3 t2 e ct) (Clos t1' e') = eval1 t2 0 e (Cont4 t1' e' ct)
appK1 (Cont4 t1' e' ct) val = eval1 t1' 0 (val:e') ct
appK1 (Cont5 t2 e ct) (Val n) = eval1 t2 0 e (Cont6 (Lit n) ct)
appK1 (Cont6 (Lit n) ct) (Val m) = appK1 ct (Val (m + n))
appK1 (Cont7 ct) (Quot t') = appK1 ct (Quot (Abs t'))
appK1 (Cont8 ct) (Quot t') = appK1 ct (Quot (Next t'))
appK1 (Cont9 ct) (Quot t') = appK1 ct (Quot (Prev t'))
appK1 (Cont10 t2 l e ct) (Quot t1') = eval1 t2 l e (Cont11 t1' ct)
appK1 (Cont11 t1' ct) (Quot t2') = appK1 ct (Quot (App t1' t2'))
appK1 (Cont12 t2 l e ct) (Quot t1') = eval1 t2 l e (Cont13 t1' ct)
appK1 (Cont13 t1' ct) (Quot t2') = appK1 ct (Quot (Add t1' t2'))
接著，是第二個deriving的步驟。
我們現在想要把eval當作是一個compiler，並把appK的部份當作VM。
所以我們需要把compile-和run-time的參數分開來處理，
然後讓eval回傳一個run-time computation。
因此，我們對eval1做一次currying transformation。
不過這裡有個需要選擇的問題，
我們需要決定哪個參數是compile-time就有的，而哪個參數是run-time才需要的。
Term明顯是compile-time，env和Cont都是run-time，所以真的有疑問的其實只有Level。
我們可以選擇將Level當作compile-time information
eval2 :: Term -> Int -> (Env -> Cont -> Val)
或是當作run-time information
eval2 :: Term -> (Int -> Env -> Cont -> Val)
如果選擇前者，那就表示說對於同一個input term，有可能會產生出不一樣的結果。
如此一來就不是uniform compilation，所以我們這裡選擇後者以做出一個uniform compiler。
先嫌棄一下(Int -> Env -> Cont -> Val)，它看起來太長了。
我們幫那一串取個一名字Compt，表示run-time computation。
type Compt = Int -> Env -> Cont -> Val
eval2 :: Term -> Compt
eval2 (Lit n) = /l e k -> if (l==0)
then appK2 k (Val n)
else appK2 k (Quot (Lit n))
eval2 (Var n) = /l e k -> if (l==0)
then appK2 k (e!!n)
else appK2 k (Quot (Var n))
eval2 (Abs t) = /l e k -> if (l==0)
then appK2 k (Clos t e)
else eval2 t l (shiftE l e) (Cont7 k)
eval2 (Next t) = /l e k -> if (l==0)
then eval2 t 1 e (Cont1 k)
else eval2 t (l+1) e (Cont8 k)
eval2 (Prev t) = /l e k -> if (l==1)
then eval2 t 0 e (Cont2 k)
else eval2 t (l-1) e (Cont9 k)
eval2 (App t1 t2) = /l e k -> if (l==0)
then eval2 t1 0 e (Cont3 t2 e k)
else eval2 t1 l e (Cont10 t2 l e k)
eval2 (Add t1 t2) = /l e k -> if (l==0)
then eval2 t1 0 e (Cont5 t2 e k)
else eval2 t1 l e (Cont12 t2 l e k)
appK2 :: Cont -> Val -> Val
appK2 = appK1
接著是deriving的第三個步驟。
我們現在再一次的嫌棄那個eval2的lambda function很難看。
所以又再對舊有的computation那個部份做一次defunctionalze。
和剛剛的Cont一樣，我們現在要把
type Compt = Int -> Env -> Cont -> Val
改成
data Compt = Compt0 | Compt1 ... | ...
不過這裡我們稍微多做一點調整。
因為我們希望compile出來的computation是一串的low-level code，
而這串computation是由instruction構成。
所以稍微改成這樣：
type Compt = [Inst]
data Inst = Inst0 | Inst1 .. | ...
並且，現在closure裡面也不是term而是compt了，所以appK裡面也需要調整一下。
eval3 :: Term -> Compt
eval3 (Lit n) = (Compt0 n):[]
eval3 (Var n) = (Compt1 n):[]
eval3 (Abs t) = (Compt3 (eval3 t)):[]
eval3 (Next t) = Compt4:(eval3 t)
eval3 (Prev t) = Compt5:(eval3 t)
eval3 (App t1 t2) = (Compt6 (eval3 t2)):(eval3 t1)
eval3 (Add t1 t2) = (Compt7 (eval3 t1)):(eval3 t2)
appC3 :: Compt -> Int -> Env -> Cont -> Val
appC3 [Compt0 n] 0 e ct = appK3 ct (Val n)
appC3 [Compt0 n] l e ct = appK3 ct (Quot (Lit n))
appC3 [Compt1 n] 0 e ct = appK3 ct (e!!n)
appC3 [Compt1 n] l e ct = appK3 ct (Quot (Var n))
appC3 [Compt3 cp] 0 e ct = appK3 ct (Clos cp e)
appC3 [Compt3 cp] l e ct = appC3 cp l (shiftE l e) (Cont7 ct)
appC3 (Compt4:cp) 0 e ct = appC3 cp 1 e (Cont1 ct)
appC3 (Compt4:cp) l e ct = appC3 cp (l+1) e (Cont8 ct)
appC3 (Compt5:cp) 1 e ct = appC3 cp 0 e (Cont2 ct)
appC3 (Compt5:cp) l e ct = appC3 cp (l-1) e (Cont9 ct)
appC3 ((Compt6 cp2):cp1) 0 e ct = appC3 cp1 0 e (Cont3 cp2 e ct)
appC3 ((Compt6 cp2):cp1) l e ct = appC3 cp1 l e (Cont10 cp2 l e ct)
appC3 ((Compt7 cp1):cp2) 0 e ct = appC3 cp1 0 e (Cont5 cp2 e ct)
appC3 ((Compt7 cp1):cp2) l e ct = appC3 cp1 l e (Cont12 cp2 l e ct)
appK3 :: Cont -> Val -> Val
appK3 (Cont0) val = val
appK3 (Cont1 ct) (Quot tm) = appK3 ct (Quot tm)
appK3 (Cont2 ct) (Quot tm) = appK3 ct (Quot tm)
appK3 (Cont2 ct) (Val n) = appK3 ct (Quot (Lit n))
appK3 (Cont3 cp2 e ct) (Clos cp1' e') = appC3 cp2 0 e (Cont4 cp1' e' ct)
appK3 (Cont4 cp1' e' ct) val = appC3 cp1' 0 (val:e') ct
appK3 (Cont5 cp2 e ct) (Val n) = appC3 cp2 0 e (Cont6 (Lit n) ct)
appK3 (Cont6 (Lit n) ct) (Val m) = appK3 ct (Val (m + n))
appK3 (Cont7 ct) (Quot t') = appK3 ct (Quot (Abs t'))
appK3 (Cont8 ct) (Quot t') = appK3 ct (Quot (Next t'))
appK3 (Cont9 ct) (Quot t') = appK3 ct (Quot (Prev t'))
appK3 (Cont10 cp2 l e ct) (Quot t1') = appC3 cp2 l e (Cont11 t1' ct)
appK3 (Cont11 t1' ct) (Quot t2') = appK3 ct (Quot (App t1' t2'))
appK3 (Cont12 cp2 l e ct) (Quot t1') = appC3 cp2 l e (Cont13 t1' ct)
appK3 (Cont13 t1' ct) (Quot t2') = appK3 ct (Quot (Add t1' t2'))
以上，我們有一個compiler，它會把source-level code compile成low-level code。
然後我們還有一台VM，它會拿compile好的low-level code並且執行，
最後再產生出source-level的code作為另一個可執行的program。
例如說：
eval3 (Next (Abs (Prev (Lit 5))))
=> [Enter,Lambda [Leave,Number 5]]
appC3 (eval3 (Next (Abs (Prev (Lit 5))))) 0 [] Cont0
=> Quot (Abs (Lit 5))
不過這樣有個小問題，那就是我們要用VM跑第二次之前就必須再compile一次。
這樣多執行的compile當然會浪費很多效率。
而如果VM產生出來的不是source-level code而是low-level code，
那之後就不會需要再重新compile，我們只需要compile一次，然後一直拿VM去跑就好。
所以我們第四個步驟就是要修改現在的VM，讓它產生的是low-level code。
同時，我們賦予Inst和Cont的constructor新的名字，讓它們更好被閱讀及理解。
另外，還有一點額外的問題要解決。
第一點，因為我們希望VM產生的結果是low-level code，
這表示說用來表示value的Val需要重寫：
data Val = Clos Compt Env | Quot Compt | Val Int
而因為現在Quot裡面包的不再是term而是low-level code，也就是compt，
所以針對term而寫的shift就不能再用了，取而代之的是shift_compt和shift_inst。
第二點，因為我們現在用compt表示所有run-time的行為，
所以Cont的各個Constructor也不應該在需要Term，而是需要Compt。
最後一點，我們關注我們的VM中哪些地方是會產生source-level code的，
接著，我們手動把這些地方改成low-level code的形式。
例如說
appK3 (Cont2 ct) (Val n) = appK3 ct (Quot (Lit n))
就改成
appK4 (Unquote ct) (Val n) = appK4 ct (Quot [Number n])
以上這些全部調整調整修改修改，就成了最後我們要的東西：
一個Uniform Compiler還有一台VM with Low-Level Code Generation。
這全部的code太長了，所以放到下面的例子之後再列出來。
我們先來看一點簡單的展示用例子：
首先這邊先define一點東西來用一下：
deq :: Val -> Compt
deq (Quot cp) = cp
run :: Compt -> Val
run cp = appC4 cp 0 [] Helf
run2 :: Compt -> Val
run2 = run.deq.run
run3 :: Compt -> Val
run3 = run.deq.run2
compile :: Term -> Compt
compile = eval4
exp72 = (Next (Next (App (Abs (Prev (Prev (Add (Lit 11) (Lit 13))))) (Prev (App (Abs (Var 0)) (Next (Next (Add (Lit 1) (Lit 3)))))))))
接個來看我們的例子：
compile exp72
=>[Enter,Enter,Push [Leave,Push [Enter,Plus [Number 1],Number 3],Lambda [Access 0]],Lambda [Leave,Leave,Plus [Number 11],Number 13]]
然後執行第一次，第二次和第三次：
(run.compile) exp72
=> Quot [Enter,Push [Leave,Push [Enter,Plus [Number 1],Number 3],Lambda [Access 0]],Lambda [Leave,Number 24]]
(run2.compile) exp72
=> Quot [Push [Plus [Number 1],Number 3],Lambda [Number 24]]
(run3.compile) exp72
=> Val 24
最後，補上整個最後的compiler/VM code：
data Term = Lit Int
| Var Int
| Add Term Term
| Abs Term
| App Term Term
| Next Term
| Prev Term
deriving Show
data Val = Clos Compt Env
| Quot Compt
| Val Int
deriving Show
type Env = [Val]
type Compt = [Inst]
data Inst = Number Int
| Access Int
| Lambda Compt
| Push Compt
| Enter
| Leave
| Plus Compt
deriving Show
data Cont = Helf
| Quote Cont
| Unquote Cont
| EvArg Compt Env Cont
| EvBody Compt Env Cont
| EvAddFst Compt Env Cont
| EvAddSnd Compt Cont
| QAbs Cont
| QNext Cont
| QPrev Cont
| QApp' Compt Int Env Cont
| QApp Compt Cont
| QAdd' Compt Int Env Cont
| QAdd Compt Cont
shiftE :: Int -> Env -> Env
shiftE _ [] = []
shiftE l (x:xs) = case x of
(Clos cp e) -> (Clos (shift_compt 0 l cp) e) : (shiftE l xs)
(Quot cp) -> (Quot (shift_compt 0 (l-1) cp)) : (shiftE l xs)
(Val n) -> (Val n) : (shiftE l xs)
shift_compt :: Int -> Int -> Compt -> Compt
shift_compt j l = map (shift_inst j l)
shift_inst :: Int -> Int -> Inst -> Inst
shift_inst j l (Number n) = Number n
shift_inst j l (Access n) = case (n >= j) && (l == 0) of
True -> Access (n+1)
False -> Access n
shift_inst j l (Lambda cp) = Lambda (shift_compt (j+1) l cp)
shift_inst j l (Push cp) = Push (shift_compt j l cp)
shift_inst j l (Enter) = Enter
shift_inst j l (Leave) = Leave
shift_inst j l (Plus cp) = Plus (shift_compt j l cp)
eval4 :: Term -> Compt
eval4 (Lit n) = (Number n):[]
eval4 (Var n) = (Access n):[]
eval4 (Abs t) = (Lambda (eval4 t)):[]
eval4 (Next t) = Enter:(eval4 t)
eval4 (Prev t) = Leave:(eval4 t)
eval4 (App t1 t2) = (Push (eval4 t2)):(eval4 t1)
eval4 (Add t1 t2) = (Plus (eval4 t1)):(eval4 t2)
appC4 :: Compt -> Int -> Env -> Cont -> Val
appC4 [Number n] 0 e ct = appK4 ct (Val n)
appC4 [Number n] l e ct = appK4 ct (Quot [Number n])
appC4 [Access n] 0 e ct = appK4 ct (e!!n)
appC4 [Access n] l e ct = appK4 ct (Quot [Access n])
appC4 [Lambda cp] 0 e ct = appK4 ct (Clos cp e)
appC4 [Lambda cp] l e ct = appC4 cp l (shiftE l e) (QAbs ct)
appC4 (Enter:cp) 0 e ct = appC4 cp 1 e (Quote ct)
appC4 (Enter:cp) l e ct = appC4 cp (l+1) e (QNext ct)
appC4 (Leave:cp) 1 e ct = appC4 cp 0 e (Unquote ct)
appC4 (Leave:cp) l e ct = appC4 cp (l-1) e (QPrev ct)
appC4 ((Push cp2):cp1) 0 e ct = appC4 cp1 0 e (EvArg cp2 e ct)
appC4 ((Push cp2):cp1) l e ct = appC4 cp1 l e (QApp' cp2 l e ct)
appC4 ((Plus cp1):cp2) 0 e ct = appC4 cp1 0 e (EvAddFst cp2 e ct)
appC4 ((Plus cp1):cp2) l e ct = appC4 cp1 l e (QAdd' cp2 l e ct)
appK4 :: Cont -> Val -> Val
appK4 (Helf) val = val
appK4 (Quote ct) (Quot cp) = appK4 ct (Quot cp)
appK4 (Unquote ct) (Quot cp) = appK4 ct (Quot cp)
appK4 (Unquote ct) (Val n) = appK4 ct (Quot [Number n])
appK4 (EvArg cp2 e ct) (Clos cp1' e') = appC4 cp2 0 e (EvBody cp1' e' ct)
appK4 (EvBody cp1' e' ct) val = appC4 cp1' 0 (val:e') ct
appK4 (EvAddFst cp2 e ct) (Val n) = appC4 cp2 0 e (EvAddSnd [Number n] ct)
appK4 (EvAddSnd [Number n] ct) (Val m) = appK4 ct (Val (m + n))
appK4 (QAbs ct) (Quot cp') = appK4 ct (Quot [Lambda cp'])
appK4 (QNext ct) (Quot cp') = appK4 ct (Quot (Enter:cp'))
appK4 (QPrev ct) (Quot cp') = appK4 ct (Quot (Leave:cp'))
appK4 (QApp' cp2 l e ct) (Quot cp1') = appC4 cp2 l e (QApp cp1' ct)
appK4 (QApp cp1' ct) (Quot cp2') = appK4 ct (Quot ((Push cp2'):cp1'))
appK4 (QAdd' cp2 l e ct) (Quot cp1') = appC4 cp2 l e (QAdd cp1' ct)
appK4 (QAdd cp1' ct) (Quot cp2') = appK4 ct (Quot ((Plus cp1'):cp2'))
