跳轉到

2019：Lean 4 構想與自舉宣言——編譯器以 Lean 撰寫#

事件#

2019 年，Leonardo de Moura 發表 Lean 4 的設計論文 （〈The Lean 4 compiler and programming language〉），並公開 Lean 4 原型。核心宣言：Lean 4 的編譯器、elaborator、宏系統全部以 Lean 本身 撰寫（自舉 self-hosting），只有極小的 runtime 以 C 撰寫。

為何重要#

  • 自舉（self-hosting）：Lean 3 的 elaborator 是數萬行 C++， 只有少數人能修改；Lean 4 讓整個系統回到 Lean 本身—— 用戶寫的 tactic、宏與編譯器內部用同一套 API。
  • 性能問題的解方：Lean 3 的 elaborator 慢且難改；Lean 4 把 elaborator 寫成 Lean 程式，配上一個高效直譯器與 C runtime， 編譯 Lean 本身的速度反而更快。
  • 宏與元程式設計合一：syntax/macro_rules/elab—— 語法擴充成為一等公民，補足 Lean 3「tactic 與語法擴充分裂」的缺陷。
  • de Moura 加入 AWS（2021 前夜）：AWS 贊助 Lean 的長期發展， 為 2023 年 Lean FRO 鋪路。

理論與實用原因#

  • 理論原因：自舉是語言成熟的終極考驗——編譯器本身就是 這門語言最大型的程式；元程式設計與宿主語言同一套理論 （引號 quasiquote、衛生宏），避免兩套語義。
  • 實用原因：Lean 3 的 C++/Haskell 混合程式碼讓貢獻門檻極高； 用戶要自訂 tactic 得學 C++。自舉後「學會 Lean = 能改編譯器」。

程式範例#

Lean 4 的宏系統——語法擴充與宿主語言同一套：

-- syntax：宣告新語法；macro_rules：語法展開
syntax "trivial" : tactic
macro_rules
  | `(tactic| trivial) => `(tactic| rfl)   -- trivial 展開成 rfl

example (n : Nat) : n + 0 = n := by trivial

-- 自訂記法：階乘
syntax:max lhs:60 "!" : term   -- 後綴運算子
macro_rules
  | `($e!) => `(Nat.factorial $e)

#eval 5!   -- 120

elab——直接操作元層（Lean 4 的 tactic 就是 Lean 程式）：

open Lean Elab Term in
elab "my_nat_lit" : term => do
  let n := 42
  elabTerm (quote n) none   -- 元層與目標層同一套語言
#eval my_nat_lit   -- 42

do 記法與 monad——Lean 4 的 do 記法支援 for/while/mut：

-- Lean 4：do 記法裡可以有可變變數與迴圈（編譯成遞迴）
def sum (n : Nat) : Nat := Id.run do
  let mut s := 0
  for i in [0:n] do
    s := s + i
  return s
#eval sum 10   -- 45

-- Lean 3 的等價寫法（對照）：只能用尾遞迴，無 mut/for
-- def sum3 : Nat → Nat
--   | 0 => 0
--   | n + 1 => n + 1 + sum3 n

C runtime 的極小化——Lean 4 的執行期只有千餘行 C：

/* Lean 4 runtime 的精神：極小、可審計、只管物件表示與 GC */
/* 編譯器本體（elaborator、kernel 前端）全部是 Lean 程式 */

對照：Lean 3 的元程式設計缺陷：

-- Lean 3：tactic 是 tactic monad + C++ API 的薄包裝，
-- 語法擴充與 tactic 分屬兩個世界，寫自訂 tactic 要學 C++ API
-- meta def my_tac : tactic unit := do ...   -- 能力受限

彌補了什麼缺陷#

彌補了 Lean 3「elaborator 是 C++ 黑箱、元程式設計受限、 效能與可擴充性矛盾」的缺陷——Lean 4 用自舉 + 元程式設計合一 + 極小 C runtime，同時解決三者。

相關條目#