跳轉到

2025：函數式程式語言的未來展望#

事件#

2025 年回顧，函數式程式設計已不再是學院內的支流：不可變性、代數資料型別、pattern matching、型別驅動開發全面滲透主流語言；依值型別與定理證明器（以 Lean 為首）與 AI 結合，正在改寫數學與軟體驗證的工作方式；effect systems、WebAssembly、多核執行環境則為函數式語言開闢新的戰場。

語法/特性加入的理論與實用原因#

1. 函數式概念的全面滲透#

  • Rust：ownership/borrowing 可視為對「記憶體安全的函數式不變量」的線性型別工程化（理論上承襲 linear types 與 region inference）；enum + match 即代數資料型別 + pattern matching。
  • Swift：value semantics、enum with associated values、Result、async/await——不可變為預設的語義來自 Clojure 以來的風潮。
  • Kotlin / Java：records（JEP 395/440）、sealed types（JEP 409）、pattern matching for switch（JEP 441）——Java 正在補上 1970 年代 ML 就有的 ADT 與 pattern matching。
  • C++：std::optional、std::variant、std::expected（C++23）、ranges（C++20）——以函式庫補上代數資料型別與組合子風格。
  • TypeScript：discriminated unions 與 exhaustiveness checking，即 ML 型別系統的 TypeScript 化。
  • 理論原因：代數資料型別與 pattern matching 有明確的型別論基礎且易於形式化。
  • 實用原因：以資料建模取代繼承層次，編譯器可檢查窮舉性，重構安全。
  • 彌補缺陷：物件導向的 null、繼承、side effect 問題。
// Java 21：ADT + pattern matching
sealed interface Shape permits Circle, Rect {}
record Circle(double r) implements Shape {}
record Rect(double w, double h) implements Shape {}

double area(Shape s) {
    return switch (s) {
        case Circle c -> Math.PI * c.r() * c.r();
        case Rect r   -> r.w() * r.h();
    };  // 編譯器保證窮舉
}

Rust 的 enum + match 同樣是 ML 式的 ADT 與窮舉檢查，所有權則是線性型別的工程化：

// Rust：enum（ADT）+ match（pattern matching，編譯器保證窮舉）
enum Shape {
    Circle { r: f64 },
    Rect { w: f64, h: f64 },
}

fn area(s: &Shape) -> f64 {
    match s {
        Shape::Circle { r } => std::f64::consts::PI * r * r,
        Shape::Rect { w, h } => w * h,
    }  // 少寫一個變體直接編譯錯誤
}

C++ 以函式庫補上「不會當機的回傳型別」與組合子風格：

// C++23：std::expected 取代例外，ranges 提供組合子風格
std::expected<int, std::error_code> parse(std::string_view s);

auto result = parse("42")
    .transform([](int n) { return n * 2; })   // 有值才轉換
    .value_or(0);                              // 失敗給預設值，不需 try/catch

2. AI 時代的定理證明與形式化驗證#

  • 理論原因：Curry–Howard 對應使「證明」成為可機器檢查的物件；Lean 的嚴格核心為 AI 產出提供裁決基準。
  • 實用原因：2024 年 AlphaProof（Lean）達 IMO 銀牌、2025 年 Gemini Deep Think 等系統達金獎水準；mathlib 的規模使 LLM 有大量訓練語料； Terence Tao 等數學家開始日常使用 Lean 工具鏈。
  • 實用案例：可預期「AI 起草、Lean 驗證、人類審閱」將成為數學研究與關鍵軟體驗證的標準工作流程。
  • 彌補缺陷：傳統軟體測試無法證明正確性；人類審稿無法窮盡證明的每一步。

3. Effect systems（效果系統）#

  • 理論原因：把副作用編碼進型別（row polymorphism + effect rows），是 Haskell IO monad 的推廣——「不純」變成可細粒度標注的型別。
  • 實用原因：Koka（Microsoft Research，2023 年發布 Koka 3）、Unison（2023 年公開版，content-addressed code）、Roc（2020 年代活躍開發）都以效果或能力型別為核心賣點。
  • 彌補缺陷：monad transformer 堆疊的心智負擔；副作用在主流語言中不可見的問題。

Koka 把副作用編碼進函式型別，effect handler 則可攔截與改寫效果的解釋：

// Koka：副作用寫進型別（<console|e> 標注會產生哪些效果）
fun greet() : <console|e> io ()
  println("hello")

fun silence() : <e|> ()          // 攔截 console 效果，使其消失
  with handler
    handler console { println(msg) -> () }   // 效果處理器改寫 println
  greet()   // 型別層面保證：此呼叫不再有 console 效果

Unison 以內容定址（content-addressed code）與能力系統重新思考程式部署：

-- Unison：能力系統（ability）明確標注副作用，與 Koka 效果系統同理
type Console = { putStrLn : Text -> {Console,Exception} () }

greet : '{Console, Exception} ()
greet = putStrLn "hello"
-- 沒有提供 Console 能力就無法呼叫 putStrLn，副作用在型別中無所遁形

TypeScript 的 discriminated unions 以型別標記取代 null 檢查：

// TypeScript：discriminated union + 窮舉檢查
type Shape =
  | { kind: "circle"; r: number }
  | { kind: "rect"; w: number; h: number };

function area(s: Shape): number {
  switch (s.kind) {
    case "circle": return Math.PI * s.r ** 2;
    case "rect":   return s.w * s.h;
  }
}

4. WebAssembly 與多核執行環境#

  • 理論原因：WASM 的線性記憶體與能力模型天然接近函數式的資源管理觀。
  • 實用原因：OCaml 5.2（2024）帶來 multicore（effects handlers + domains）與 wasm 後端；GHC 的 WebAssembly 後端（2023 起）使 Haskell 可跑在瀏覽器；F#、Scheme（WASM GC 提案）也陸續支援。
  • 彌補缺陷：函數式語言長期難以觸及前端與沙盒環境；OCaml 長期缺乏並行原語。

OCaml 5 的 effect handler 與 domain 提供輕量並行原語：

(* OCaml 5：effect handler（multocore）——可恢復的效果 *)
type _ Effect.t += Print : string -> unit Effect.t

let main () =
  Effect.perform (Print "hello")

let () =
  try_with main ()
    { effc = fun (type a) (e : a Effect.t) ->
        match e with
        | Print s -> Some (fun (k : (unit, a) continuation) ->
            print_string s; continue k ())   -- 攔截後恢復 continuation
        | _ -> None }

總結發展主軸與預測#

自 1936 年 lambda 演算、1958 年 LISP 以來，函數式程式設計的發展主軸是「理論先於工程數十年，再逐波滲透主流」：1958–1970 年代（LISP、ML）建立 lambda、GC、巨集與型別推導；1980–1990 年代（SML、Haskell、GHC）建立純函數式與惰性求值；2000 年代（Scala、Clojure、F#）把函數式帶上 JVM 與 .NET；2010 年代（Idris、Lean）把依值型別帶入實用；2020 年代則是「函數式 + 依值型別 + AI」的三線合流。可以預測：不可變性與 ADT 將成為所有主流語言的預設；Lean 式的形式化驗證將與 LLM 共生成為軟體品質的基礎設施；effect systems 與 WASM 將孕育下一代的系統級函數式語言。

相關條目#