跳轉到

2021：Lean 4 問世——自舉編譯器與宏合一#

事件#

2021 年，Lean 4 第一個里程碑版本（v4.0.0-m 系列）問世， 2023 年正式發佈 v4.0.0 穩定版。Lean 4 是一場豪賭： 整個編譯器、elaborator、宏系統、LSP server 全部以 Lean 撰寫， 只有約千餘行的 C runtime。

為何重要#

  • 自舉編譯器：Lean 3 的 elaborator 是數萬行 C++； Lean 4 讓整個系統回到 Lean——修 bug、加功能、寫 tactic 都是「寫 Lean 程式」。
  • syntax/macro_rules/elab 三層宏系統：
  • syntax：宣告語法（解析器）
  • macro_rules：語法展開（巨集）
  • elab：直接操作元層（完整的編譯器 API） 補足 Lean 3「語法擴充與元程式設計分裂」的缺陷。
  • 衛生宏（hygienic macros）：宏產生的識別字不會與用戶程式 意外衝突——沿襲 Scheme 衛生宏傳統，用 quasiquote 實現。
  • do 記法升級：支援 mut、for、while，編譯成遞迴； monad 內聯（restrict monad）讓 do 記法接近命令式速度。
  • structure eta 成為核心：結構值相等由欄位決定（Lean 2/3 是可選）， 讀取類型別的語義更自然。
  • 增量編譯（incremental recompilation）：改一個定義只需重編譯 依賴它的部分——LTE 等大型專案的救星。

理論與實用原因#

  • 理論原因：自舉是語言自指的最高驗證——編譯器本身就是 這門語言最大型的程式；衛生宏的理論（quasiquote、hygiene， Kohlbecker 1986）保證宏不破壞 α-等價。
  • 實用原因：Lean 3 的 C++/Haskell 混合程式碼讓貢獻門檻極高； 數學社群需要效能與可擴充性——自舉 + 增量編譯同時解決。

程式範例#

三層宏系統——語法擴充是一等公民：

-- 第一層：syntax 宣告新語法
syntax "print_hello" : command
-- 第二層：macro_rules 展開成既有語法
macro_rules
  | `(print_hello) => `(#eval "hello")

print_hello

-- 第三層：elab 直接操作元層
open Lean Elab Command in
elab "my_version" : command => do
  logInfo s!"running on Lean {Lean.versionString}"
my_version

衛生宏——宏的識別字不會外洩：

-- 宏內部的 temp 與用戶的 temp 不衝突（衛生）
syntax "swap_demo" : term
macro_rules
  | `(swap_demo) => `(let temp := 1; temp + 1)

def temp := 100
#eval swap_demo + temp   -- 2 + 100 = 102，宏的 temp 沒有污染

do 記法與可變狀態——命令式風格，編譯成遞迴：

-- Lean 4：mut/for/while 直接可用
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

def fibIter (n : Nat) : Nat := Id.run do
  let mut (a, b) := (0, 1)
  for _ in [0:n] do
    (a, b) := (b, a + b)
  return a
#eval fibIter 30   -- 832040，接近命令式速度

structure eta——結構相等由欄位決定：

structure Point where
  x : Nat
  y : Nat

theorem eta (p : Point) : Point.mk p.x p.y = p := rfl
-- Lean 4 中這是核心規則；範疇論裡「等價物件的細粒度推理」依賴它

依賴型別驗證的程式——規格寫進型別：

-- 用依賴型別保證「長度不變」
def safeTail : {n : Nat} → Vector Nat (n+1) → Vector Nat n
  | _, .cons _ xs => xs

-- partial def：允許無法（或不想）證明終止的定義
partial def spin (n : Nat) : Nat := spin n  -- 編譯器接受

對照：Python 的型別缺陷——規格無法進型別，執行期才爆：

def tail(xs: list) -> list:   # 長度為 0 會 silently 出錯
    return xs[1:]             # IndexError，執行期才爆

彌補了什麼缺陷#

彌補了 Lean 3「elaborator 是 C++ 黑箱、語法擴充與元程式設計分裂、 大型專案增量編譯缺失」的缺陷——Lean 4 用自舉、三層宏系統、 structure eta 與增量編譯，讓「證明助手」正式成為「通用程式語言」。

相關條目#