Lean言語は新世代の純粋関数型言語になれるか？

関数型まつり2025で発表したスライドです。

1. Lean言語は 新世代の純粋関数型言語になれるか？ Proxima Technology 井上亜星
2. Lean 言語ってなに？ 2013年ごろに当時 Microsoft Research に在籍し ていた Leonardo de Moura 氏により開発が始め られた定理証明支援系。 Rocq(旧Coq) や Agda と同様に、依存型という 強力な型システムのパワーによって命題を表現 し、証明することを可能にしている。 現在、Lean 4 がアクティブに開発中。
3. 他の定理証明支援系とどう違うの？ 大きく分けて２つの特徴があります １．依存型に基づく定理証明支援系であると同時に、 純粋関数型言語でもある （プログラミングと証明を両立するための工夫もある） ２．強力なメタプログラミングフレームワークを備えている
4. 純粋？Haskell みたいな言語ってこと？ 確かに Haskell にかなり影響を受けている （モナドや do 構文もある） しかし、Haskell にはなかったおもしろい機能がある： ・notebook なしでもフィードバックが即座に得られる ・do 構文が強力で、for ループや while ループも書ける ・フィールド記法があって、関数適用をフィールドアクセスのように書ける ・効率的に計算ができるようにする Functional but in-place という仕様がある
5. フィードバックが即座に得られる エディタ上で編集するごとに実行結果を確認できる 画像では Error Lens 拡張機能を使用しています
6. 強力な do 構文 ・for ループと while ループ ・let mut で可変なローカル変数 ・continue と break 詳細は ‘do’ unchained という論文を参照
7. フィールド記法 T が e の型であるときに、関数適用 T.f e を e.f と書くことができる
8. Functional but in-place 他で参照されていない値を更新するとき、自動で破壊的な更新が行われる (参照カウントに基づく)
9. 他の定理証明支援系とどう違うの？ 大きく分けて２つの特徴があります １．定理証明支援系であると同時に、純粋関数型言語でもある （プログラミングと証明を両立するための工夫もある） ２．強力なメタプログラミングフレームワークを備えている
10. プログラミングと証明を両立するために 実装と論理モデルを分離することができる ・自然数 Nat は、論理モデルはペアノの公理で与えられているが、 　実際の計算は別の高速な方法で行われる ・文字列 String は Char のリストとして定義されているが、 　実際の計算は別の高速な方法で行われる などなど…。 正当性の証明付きで置換することもできるし、証明なしで置換することもできる
11. 他の定理証明支援系とどう違うの？ 大きく分けて２つの特徴があります １．定理証明支援系であると同時に、純粋関数型言語でもある （プログラミングと証明を両立するための工夫もある） ２．強力なメタプログラミングフレームワークを備えている
12. 強力なメタプログラミングフレームワークとは？ syntax コマンドと declare_syntax_cat コマンドでパーサを書き換えて新しい構文を定義す ることができるほか、macro_rules コマンドでマクロも自由に書ける
13. 実際にプログラムを書けるのか？ 実際に Lean で書かれた（広く使われている）プログラムの例として、 ドキュメント生成ツール doc-gen4 や文書作成ツール verso がある。 実際、Lean の公式マニュアルは verso を使って書かれている。
14. まとめ Lean 言語というプログラミング言語があって、 • Rocq (旧 Coq) のように定理証明支援系として使える • Haskell のように純粋関数型言語としても使える 後発言語らしい工夫もあり • 定理証明とプログラミングを両立する工夫 • 純粋関数型言語のパフォーマンス面・ＵＩ面双方の欠点を改善
15. 自己紹介 名前：井上亜星 所属：Proxima Technology GitHub 等ネットでは 北窓（きたまど） という名前でやってます
16. 自己紹介 n 月刊ラムダノートに記事を寄稿したほか、 Lean by Example というオンラインリファレンスを書いてます
17. おわりに lean-ja という Lean の日本語コミュニティ （Discordサーバ）もあります。 ご興味があればぜひ。
18. ご清聴ありがとうございました