# 改善可能なプログラミング言語について ## 1. 「改善可能（Perfectable）」の定義 プログラミング言語における「改善可能」という概念を明確に定義します。この用語は、単なる不完全性の是正ではなく、以下の観点から言語の質的向上の可能性が示唆される状態を指します： - 学習のしやすさ（オンボーディング体験の最適化） - セーフティ保証の強化（メモリ安全性、並行実行の信頼性など） - パフォーマンス最適化の容易さ ## 2. 既存言語の評価と限界 現在存在する主要なプログラミング言語を簡潔に検討し、「完璧」または「近似的に完璧」という状態に至るにおける課題を分析します： - **静的型付け言語**: タイプ推論の複雑さと型安全性のバランスが困難。 - **動的型付け言語**: 実行時のエラー防止とパフォーマンスのトレードオフが存在。 - **メモリ管理**: ガベージコレクタによるオーバーヘッドや、明示的なメモリアロケーションの煩雑さ。 ## 3. 「改善可能」な言語のための主要特徴 「改善可能」という属性を満たすための本質的な機能を以下のように整理します： - **低摩擦な静的型付け**: コンパイラーと開発者の対話を最小限に抑えつつ、型安全性を確保する仕組み。 - **オーバヘッドなしのメモリ安全性**: ガベージコレクタを不要としながら、安全なメモリ管理を実現する技術。 - **明確なエラー報告とユーティリティツール**: エラーメッセージの解釈可能性が高く、デバッグプロセスを支援する統合環境。 ## 4. 実装戦略への考察 such a language の設計に向けた潜在的アプローチを検討します： - 既存コンパイラ技術の活用（例: LLVM や Rust のバースト最適化技術の拡張） - 新しい構文規則やドメイン固有の構造体の導入 - セマンティクスとシンタックスの再考による言語パルタイン設計 ## 5. トレードオフの評価 「完璧」に至るためには、以下のバランスを慎重に評価する必要があります： - シンプルさと表現力の調和 - 開発者の生産性と実行パフォーマンスの関係性 - セーフティ保証と柔軟性の両立

パーティーの席上で、シドニー・フォン・アックスに「40 のプログラミング言語を挙げてくれ」と問われた。いやあ、そのレベルならあなたも Bayesian だね。

• Racket
• Agda
• Clean
• Elm
• TypeScript
• SH
• ASP
• Verilog
• JavaScript
• Scheme
• Rust
• Nim
• Intercal
• SED
• Isabelle
• Visual Basic
• Zsh
• Alokscript
• Coq
• Idris
• Hack
• Prolog
• Whitespace
• PureScript
• Go
• Odin
• Haskell
• Python
• TCsh
• Unison
• Clingo
• Bash
• Java
• Zig
• Cyclone
• PHP
• AWK
• C
• ActionScript
• C++

でも、最高なのは Lean だ。

なぜなら？
完璧化可能だからだ。現時点で完璧ではないにせよ、「完璧化可能」であることは確かだ。Lean の性質を、そのまま Lean で記述できる。これらの事実や性質の体系全体を「進歩」と呼ぼう。

いかなる言語においても、やがてはコードそのものに関する言明をしたくなるものだ。例えば「必ず 5 を返す関数」があっても、ほとんどすべての言語では、その事実を活用して言語自身が助けてくれるような使い方はできにくい：

function returnFive(x : number) : number {
  return 5;
}

対照的に Lean では：

def returnFive (unused variable `x` : Int) : Int := 5

theorem returnFive_eq_five (x : Int) : returnFive x = 5 := rfl

example (a : Int) : 6 = returnFive a + 1 := by
  unfold returnFive
  rfl

すべてのゴール達成！🐙

型を持たない言語も、PHP 7.4 や Python の型アノテーションに見られるように、「型を追加しよう」とする方向へと進化する傾向にある。必然的に人々は「型を推し進めたい」と考えるのだ。Go や C++テンプレートはその代表例であり、「コンパイル時に計算可能なら、いつか誰かがそうしたいだろう」という思いが裏打ちされている（Rust の継続的な constification がその現れだ）。

しかし、あらゆることを「適切に」行うのが最も簡単で、それが本質的には依存型のことだ。それ以上の複雑な概念もあるが、チューリング完全性という観点から言えば、依存型だけでも十分に到達点へ導き得る。つまり「完璧化可能」なのである。

さらに型の上に、2 つの型の等しさ・不等しさを検証するためのインフラストラクチャが必要になる。これは本質的に定理証明器のことだ。依存型を持つ言語はすべて定理証明器として機能し得るが、美しい API（我々が呼び出す「定理証明インフラストラクチャ」と呼ぶ）を育まなければならない。それが物語の半分であり、それは意味論の側面である。もう半分はシンタックスで、メタプログラミングおよびカスタムシンタックスによるものだ。

メタプログラミング

多くの言語ではこの機能が存在しないか、Rust のプロシージャルマクロのようにややぎこちないものである。Lean では驚くほどシームレスだ。以下はカスタムボード表記付きの将棋（※実際にはタイコタクトー／井戸川将棋風）の実装例：

/-- 将棋の二人プレイヤー -/
inductive Player where
  | X
  | O
  deriving BEq, Inhabited

/-- ボード上のマス：空か、プレイヤーが配置された状態 -/
inductive Square where
  /-- まだ誰もこのマスに置いたわけではない。 -/
  | empty
  /-- プレイヤーがそのマスを確保している。 -/
  | occupied (player : Player)
  deriving BEq, Inhabited

@[simp] def boardSize : Nat := 9

/-- 3x3 の将棋ボード -/
structure Board where
  squares : Array Square
  deriving BEq

次にカスタムシンタックス：

/-- ボードリテラル内のセル：`X`, `O`, または `_（空）` -/
declare_syntax_cat tttCell
syntax "X" : tttCell
syntax "O" : tttCell
syntax "_" : tttCell

/-- 「|」で区切られた 3 セルの一行 -/
declare_syntax_cat tttRow
syntax (name := tttRowRule) tttCell "|" tttCell "|" tttCell : tttRow

/-- 3 行が構成する完全な 3x3 ボード -/
declare_syntax_cat tttBoardSyntax
syntax tttRow tttRow tttRow : tttBoardSyntax

/-- 単一のセルを `Square` に展開する。 -/
private def elabTttCell (stx : Lean.Syntax) : Lean.Elab.Term.TermElabM Square :=
  match stx with
  | `(tttCell| X) => pure (.occupied .X)
  | `(tttCell| O) => pure (.occupied .O)
  | `(tttCell| _) => pure .empty
  | _             => Lean.throwError s!"unsupported cell syntax {stx}"

open Lean Elab Term in
/-- `board!` は可視的なボード配置をコンパイル時に `Board` に変換する。
    各セルは展開段階で検証される。 -/
elab "board! " b:tttBoardSyntax : term => do
  let mut squares : Array Square := #[]
  unless b.raw.getNumArgs = 3 do
    Lean.throwError s!"Expected 3 rows, got {b.raw.getNumArgs}"
  for rowIdx in [:3] do
    let row := b.raw.getArg rowIdx
    unless row.isOfKind `tttRowRule do
      Lean.throwError s!"malformed tttRow"
    let cells := #[row.getArg 0, row.getArg 2, row.getArg 4]
    for cell in cells do
      squares := squares.push (← elabTttCell cell)
  unless squares.size = boardSize do
    Lean.throwError s!"internal error: expected 9 squares, got {squares.size}"
  let squareTerms ← squares.mapM fun sq =>
    match sq with
    | .empty => `(Square.empty)
    | .occupied .X => `(Square.occupied Player.X)
    | .occupied .O => `(Square.occupied Player.O)
  let arrSyntax ← `(#[$squareTerms,*])
  let boardTerm ← `(Board.mk $arrSyntax)
  Lean.Elab.Term.elabTerm boardTerm none

使用方法：

X | O | _
_ | X | _
O | _ | X
#eval board!

Win X

カスタムシンタックスの使用例：

X | O | _
_ | X | _
O | _ | X#eval board!

Win X

これにより、API を階層化してシンタックスの背後に隠すことが可能になる。また、その解釈は容易に切り替えられる。Lean の型システムもメタプログラミングをある程度支援する（ただし、より強力なインフラ整備のために、Lean シンタックスに関する何らかのモダリティを持つ「超メタプログラミング」を見るのが嬉しい）。

def «🎮 tic tac toe 🎮» : Board := board!
  X | O | X
  O | X | O
  X | _ | O
#eval getGameStatus «🎮 tic tac toe 🎮»
-- Win X

このようなことを「適切に」行うことは、まさに定理証明器である。定理証明はプログラミングにおける収束進化によって生み出されたものだ。

スピード

これが最大の理由だ。低速な言語はつまらない。ではなぜコンピュータを使うのか？Lean はもっと高速にできるはず。Rust 並みの速さではないが、2 つのコード片が等しいことを示す能力のおかげで、最適化のポテンシャルは非常に高い。

もし二つの関数がすべての入力に対して証明可能に等しければ、コンパイラは自由に出し入れして相互置換できる：

/-- 二つの関数がすべての入力に対して証明可能に等しければ、
    コンパイラは自由に出し入れして相互置換できる。 -/
theorem five_plus_one_eq_six : ∀ a : Int, returnFive a + 1 = 6 := by
  intro a
  unfold returnFive
  rfl

Leo de Moura もこの必要性を強く感じているらしく、後方互換性が犠牲になりつつある。幸いなことに AI の世界ではコードを書き直すのが非常に容易であり、定理証明器は究極のリファクタリングツールと言える（なぜそう考えないだろうか）。

コミュニティ

Lean はそのカテゴリにおいて実際に勢いを得ている唯一の言語だ。Coq, Idris, Agda はもう対決的な立場にはいない。Idris も理論上はプログラム言語でありつつも証明器としての側面を持つが、コミュニティが臨界点に達しなかった。F* も該当するが、そのコミュニティ規模は丸め誤差程度だ。Lean は純粋なプログラミング能力を持ちつつ定理証明器としても成長を続けているのが唯一の存在だ。

このブログ記事自体も Lean コードによって書かれている。

Eliza Zhang にちなって言う。彼女は私が 1 週間以内に標準ライブラリのみでウェブアプリを C で書けないと打賭していた。彼女は正しかった。その言葉の意味さえ理解していなかった。しかし、私は「できない」と言ったことのできない自分自身を受け入れ、それがコーディングへの入り口になった。