在什麼是CPS？我們討論過CPS是怎樣的程式風格，以及編譯器可以怎麼利用這種風格。但我們該不該使用CPS呢？這曾經引發一系列的爭論

編譯理論之爭 [local-0]

1978 RABBIT: A Compiler for SCHEME，據說這是最早採用CPS的編譯器
1992 Compiling with Continuations，Appel整理並提供了完整的ML CPS風格編譯器
1993 The essence of compiling with continuations，形式化並辨識出ANF，認為direct style (ANF) 在local control flow上提供了更簡單的工作方式
1997 A reflection on call-by-value，這篇正式的討論了direct style在什麼時候可以替代CPS編譯器
2007 Compiling with continuations, continued，Kennedy認為CPS在functional language上有勝過ANF或是monadic IR的地方，主要爭點就是inline會導致ANF需要renormalization
2017 Compiling without continuations，Haskell方認為，可以用local continuations（又稱join points）處理direct style的缺點
2019 Compiling with continuations, or without? whatever.，這篇認為我們需要重新考慮，用還是不用CPS取決於編譯器/語言的目標，而且join points無法讓optimizer有足夠的evaluation context資訊，導致冗餘的轉換。因此作者認為正確的問題應該是「我們需要什麼程度的CPS」，設計了direct style跟CPS optimizations都能運作的IR

我個人的觀點比較接近 [Whatever2019]，但傾向採用delimited continuation（並整合runtime支援），局部控制流的編譯使用direct style。這就引出了Bowman的A Low-Level Look at A-Normal Form，這篇論文主張「The traditional view of ANF that normalizing commuting conversions is hard, found in formal models and informed by high-level calculi, is wrong」。Bowman認為可以發展出一個normal form具有以下性質

容易normalizing commuting conversion
不需要join points
不需要code duplication
不需要在inline之後renormalization
容易擴展出新的lexically scoped effects

並且Bowman確立了ANF跟monadic form的關聯與intensional properties（分析abstract machine），引導出了imperative monadic form這個形式，設計出untyped lambda-calculus (with scoped regions) 可用的compiler pipeline。最後證明這樣的compiler在stack跟memory行為上都比ANF有所改善

The main take-away from this work is that, in general, monadic form should be preferred over ANF, and A-normalization should only be done in a low-level imperative intermediate form. This maximizes the advantages of each form, and avoids all the standard problems with ANF.

Definition A-normal form (ANF) [1RPZ]

ANF常被叫做administrative normal form，好像是個模糊的「把administrative redex消掉」的說法。但最好想成以下的定義：對給定的A-reductions集合，化約會得到的normal form

Lambda calculus的A-normalization可以寫成以下定義

\begin{aligned} v &::= \iota \mid x \mid (\lambda\ (x)\ e) \\ e &::= v \mid (op\ \vec{e}) \mid (e\ e) \mid (\text{let}\ (x\ e)\ e) \mid (\text{if0}\ e\ e\ e) \\ E &::= \cdot \mid (\text{let}\ (x\ E)\ e) \mid (\text{if0}\ E\ e\ e) \mid (E\ e) \mid (v\ E) \mid (op\ \vec{v}\ E\ \vec{e}) \\ O &::= v \mid op \end{aligned}

A-reductions

\begin{aligned} E[(\text{let}\ (x\ e_1)\ e_2)]\quad\rightarrow_A\quad &(\text{let}\ (x\ e_1)\ E[e_2]) \quad &A_1 \\ &\text{where}\ E \ne \cdot \\ E[(\text{if0}\ v\ e_1\ e_2)]\quad\rightarrow_A\quad &(\text{if0}\ v\ E[e_1]\ E[e_2]) \quad &A_2 \\ &\text{where}\ E \ne \cdot \\ E[(O\ \vec{v})]\quad\rightarrow_A\quad &(\text{let}\ (x'\ (O\ \vec{v}))\ E[x']) \quad &A_3 \\ &\text{where}\ E \ne \cdot, E \ne E'[(\text{let}\ (x\ \cdot)\ e)], \text{fresh}\ x' \end{aligned}

化約成的A-normal form（也就是說，不斷套用A-reductions應該讓程式變成以下形式，這些形式套用A-reductions不會再化簡）

\begin{aligned} (Values)&\quad &V &::= \iota \mid x \mid (\lambda\ (x)\ M) \\ (Computations)&\quad &N &::= V \mid (V\ V) \mid (op\ \vec{V}) \\ (Configuration)&\quad &M &::= N \mid (\text{let}\ (x\ N)\ M) \mid (\text{if0}\ V\ M\ M) \end{aligned}

我們通常會假設綁定中涉及的變數唯一且考慮 $\alpha$ -equivalence

ANF的缺點 [RG5R]

ANF可以保證每個計算都由一系列的let序列化，並且所有operands都一定是values，從而對指令語言後端編譯是好用的表示形式。但ANF也有一些缺點

ANF在 $\beta$ -reduction 下不封閉 [local-0]

ANF的缺點之一是在 $\beta$ -reduction 下不封閉，比如

(\text{let}\ (x\ ((\lambda\ (y)\ M)\ V))\ x) = (\text{let}\ (x\ M[y:=V])\ x)

但這個表達式不是合法的ANF，在RHS位置 $M[y:=V]$ 不被允許出現。這讓ANF $\beta$ -equivalence必須重新normalize所有commuting conversions

這對最佳化來說是一個缺陷，因為 $\beta$ -equivalence model了inlining optimizations；而renormalize是不便又昂貴的計算

$A_2$ 會導致程式碼指數級的增長 [local-1]

我們可以觀察以下案例套用 $A_2$ 的結果

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

因為continuation $E_1[♢]$ 是 let x := ♢ in LARGE，所以第一次轉換得到

if0 (if0 (if0 0 0 1) 0 1)
  E1[0]
  E1[1]

再來 $E_2[♢]$ 是 if0 ♢ E1[0] E1[1]，好吧，那就得到

if0 (if0 0 0 1)
  E2[0]
  E2[1]

再來 $E_3[♢]$ 是 if0 ♢ E2[0] E2[1]，所以是

if0 0
  E3[0]
  E3[1]

最後我們攤開來看就得到

if0 0
  if0 0
    if0 0
      let x := 0 in LARGE
      let x := 1 in LARGE
    if0 1
      let x := 0 in LARGE
      let x := 1 in LARGE
  if0 1
    if0 0
      let x := 0 in LARGE
      let x := 1 in LARGE
    if0 1
      let x := 0 in LARGE
      let x := 1 in LARGE

所以3層if的堆疊得到8個 LARGE

到這裡，Bowman就問說，如果ANF有這麼多問題，那麼與其去修復它，為什麼不要禁止 $A_2$ 轉換然後允許 let x := if0 V M1 M2 in M 這個形式呢？畢竟這個形式說穿了也就是

begin:
  if0 V
    set! x M1
    set! x M2
  M

這完全是指令語言後端可以接受的程式！事實上，這早就已經是實用編譯器的常見做法

A-normalization對非monadic effect不安全 [local-2]

Bowman舉了letregion作為案例，並認為沒有文獻討論過這個缺陷。注意到Bowman不想重複join point的老路，也就是要避免用local continuation處理這個問題

Join Points [Z97H]

對於 $A_2$ 規則引入的程式碼爆炸，除了直接改成用CPS，傳統方式是引入一個local continuation來處理，這種continuation常叫做join point

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

我們轉換成

let j y := LARGE
if0 (if0 (if0 0 0 1) 0 1)
  let x := 0 in j x
  let x := 1 in j x

然後以此類推，我們就不會產生重複的程式碼。然而join points也有很明顯的缺點，比如引入更多的allocation（lambda的runtime表示closure並不是免費的），並且阻止對 $j$ 的最佳化，這往往導致實務編譯器必須考慮引入相應的join points algebra去處理一系列的轉換問題

那除了CPS跟join points我們還可以怎麼辦？Bowman考慮了另一個形式monadic form，並正式處理monadic form跟ANF之間的關聯

Monadic form [UP3Y]

如果讓let表示monadic bind，讓return隱含在values下，那monadic form有以下commuting conversions

\begin{aligned} \text{let}\ (x\ U)\ E[x] &= E[U] \quad&\text{(Left Identity)} \\ \text{let}\ (x\ C)\ x &= C \quad&\text{(Right Identity)} \\ \text{let}\ (y\ (\text{let}\ (x\ C)\ C_1))\ C_2 &= \text{let}\ (x\ C)\ (\text{let}\ (y\ C_1)\ C_2) \quad&\text{(Associativity)} \\ \text{let}\ (x\ (\text{if0}\ U\ C_1\ C_2))\ C &= \text{if0}\ U\ (\text{let}\ (x\ C_1)\ C)\ (\text{let}\ (x\ C_2)\ C) \quad&\text{(Commute)} \end{aligned}

ANF可以定義成monadic form用associativity跟commute這兩條規則normalize的結果

Monadic form的缺點是沒那麼正規化，會有更多等價但不同的表達形式。有辦法同時得到A的正規化跟避免程式膨脹嗎？這就是non-strict monadic form的用途

Definition Non-strict monadic evaluation contexts與B-normalization [PIBK]

Non-strict monadic evaluation contexts $E^b$

E^b ::= \cdot \mid (\text{if0}\ E^b\ e\ e) \mid (E^b\ e) \mid (v\ E^b) \mid (op\ \vec{v}\ E^b\ \vec{e})

B-reductions

\begin{aligned} E^b[(\text{let}\ (x\ e_1)\ e_2)] \quad\rightarrow\quad &\text{let}\ (x\ e_1)\ E^b[e_2]\quad &B_1 \\ &\text{where}\ E^b \ne \cdot \\ E^b[(\text{if0}\ v\ e_1\ e_2)] \quad\rightarrow\quad &\text{let}\ (y\ (\text{if0}\ v\ e_1\ e_2)) E^b[y]\quad &B_2 \\ &\text{where}\ E^b \ne \cdot, \text{fresh}\ y \\ E^b[(O\ \vec{v})] \quad\rightarrow\quad &\text{let}\ (y\ (O\ \vec{v}))\ E^b[y]\quad &B_3 \\ &\text{where}\ E^b \ne \cdot, \text{fresh}\ y \end{aligned}

如果定義 $B = \{B_1, B_2, B_3\}$ ，那麼這組規則會確保evaluation position上的non-value會被換成value。

Example 避免程式指數爆炸成長 [local-0]

相比起 $A_2$ 規則， $B_2$ 專門用來避免程式指數爆炸的轉換。我們再次回到失敗案例然後推導變換過程

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

我們改用 $E^b[-]$ 來轉換，由於不抽取let-if，所以我們要直接處理rhs，於是

let x :=
  let y := if0 (if0 0 0 1) 0 1
  in if0 y 0 1
in LARGE

下一步

let x :=
  let z := if0 0 0 1
  in let y := if0 z 0 1
  in if0 y 0 1
in LARGE

所以這確實不會導致大量的程式碼重複

最後我們有辦法同時得到A跟B化簡的好處嗎？可以的，這就是最終形式imperative monadic form

Imperative monadic form [YI0W]

藉由分析ANF跟monadic form的機器表示的意圖，Bowman提出了Imperative monadic form。只要我們讓

let x := a
in b

等於

set! x := a
b

的別稱。在語意上commuting conversion就不再是困擾了

set! y := {
  set! x := t
  t
}
t

等於

set! x := t
set! y := t
t

箝套的if也不再是問題

set! y := if v t1 t2
t

等於

if v
  set! y := t1
  set! y := t2
t

注意到右邊幾乎已經是指令語言可以處理的形式了

Definition Syntax [local-0]

注意到為了支援對if expression的轉換，需要加入if statement

\begin{aligned} t &::= (\text{begin}\ \vec{s}\ t) \mid v \mid (\text{if0}\ v\ t\ t) \mid (\text{call}\ v\ v) \mid (op\ \vec{v}) \\ s &::= (\text{begin}\ \vec{s}) \mid (\text{set!}\ x\ v) \mid (\text{if0}\ v\ s\ s) \mid (\text{set!}\ x\ t) \mid (\text{set!}\ x\ (op\ \vec{v})) \mid (\text{set!}\ x\ (\text{call}\ v\ v)) \\ v &::= (\lambda\ (x)\ t) \mid \iota \end{aligned}

AB-normalization [UQJG]

根據Imperative monadic form我們已經可以定義AB-reduction

\begin{aligned} (\text{set!}\ x\ (\text{if0}\ v\ t_1\ t_2)) \quad&\rightarrow_{AB}\quad (\text{if0}\ v\ (\text{set!}\ x\ t_1)\ (\text{set!}\ x\ t_2)) \quad &AB_1 \\ (\text{set!}\ x\ (\text{begin}\ \vec{s}\ t)) \quad&\rightarrow_{AB}\quad (\text{begin}\ \vec{s}\ (\text{set!}\ x\ t)) \quad &AB_2 \end{aligned}

這種方案避開了join points、編譯器不需要引入整套CPS風格、也不會造成程式碼膨脹（就像B-normalization），對stack使用最佳化（就像A-normalization）。這個做法的關鍵想法在于lexical expressions一定要在A-normalize之前先轉換成循序述句表達

AB-normalization還可以根據新的effect調整，像Bowman就展示了letregion的案例

跟CPS不一樣的是，AB-normalization解決的是local control flow的commuting conversion問題，如果目的是處理non-local control flow的編譯，那CPS可能還是有用途，只是現代的編譯器更可能直接在runtime端實作需要的continuation系統，減少轉換的工作

最終pipeline [local-1]

lambda-calculus
  --> monadic form            (只有 sequencing，不碰 commuting conversion)
  --> imperative monadic form (lexical binding 降成 set!)
  --> AB-normal form          (在 statement 上做 A-normalization)

對照傳統的

lambda-calculus
  --> ANF             (sequencing + commuting conversion 一起做)
  --> code gen

傳統方法的A-normalization compiler必須寫成CPS風格（compiler自己拿一個meta-level的continuation $\kappa$ 來累積上下文），還要在target language裡處理join point的表示；而monadic版本的compiler就只是遞迴地sequence，每個子項回傳的都是可以互相組合的

沒解決的：case-of-case [local-2]

這個方法有一個缺點：我們不確定AB-normal compiler能不能處理case-of-case

(if0 (if0 e 1 0) 5 6)

ANF compiler會產生 (if0 e (if0 1 5 6) (if0 0 5 6))——分支被複製了，但接著partial evaluation一步就化簡成 (if0 e 6 5)。AB-normal compiler生出的是 (let (x (if0 e 1 0)) (if0 x 5 6))，沒有複製程式碼，但也就沒辦法做同樣的化簡

Maurer等人的join point calculus 處理這個例子處理得很好，代價是引入join point。Bowman的提議是把條件位置分離成一個boolean的sublanguage，再讓一個簡單的boolean optimizer去化簡，這是Chez的做法，表示這可能這是實務上有效的方案

§6.3談到AB normalizing也可以用monadic language配合state monad表示，不見得要做成imperative language。但這種做法用在處理多個不同effect上會導致著名的monad不可組合問題，所以就算要這麼做，可能也要考慮用單一大monad包含所有此階段需要的effect

這不是新發明，只是沒有命名 [local-3]

論文最後把幾個高效能編譯器抓出來對照，說它們早就在做AB-normalization了

Chez Scheme：L10轉換直接把let/let跟let/if的commuting conversions轉換成imperative IR
TIL（ML編譯器）的B-form是一個monadic form IR
SIL（ML to Ada compiler）

用論文自己的話說就是：這些編譯器早在這個方法被辨識出來之前就使用它了

To CPS or not to CPS：編譯理論之爭 [ASEH]