Lean日報: Lean の Batteries ライブラリの #lint コマンド
はじめに
この Lean 日報ではシリーズ記事として、Lean について新たに学んだことを書いていきます。定期更新ではありません。
Lean とは何か
Lean は、プログラミング言語の一種です。しかしただの言語ではなくて、純粋関数型プログラミング言語かつ定理証明支援系でもあるという特徴を持ちます。数学の形式化や自動証明の構成、数学的問題について推論するAIの開発などに応用が期待されています。
コマンドとは何か
まず前提として、Lean 4 ではプログラムを実行するのに Jupyter Notebook のような特別な環境を必要としません。#eval コマンドなど、特定のコマンドを実行することでエディタ内で即座にフィードバックが得られるようになっています。
この手の「Lean から対話的にフィードバックを得る」系のコマンドは # で始まることが多く、hash command と呼ばれたり diagnostic command と呼ばれたりします。私はよく「対話的コマンド」と呼んでいます。
hash command の代表的なものが、さきほども名前を挙げた #eval コマンドであり、これはその名の通り式をインタプリタに食べさせて評価します。
#lint コマンド
さて、今回は #lint コマンドについてお話します。
#lint コマンドは # から始まっていますが、お察しのように Lean から情報を得ることができるコマンドです。これはリンターを実行して結果を教えてくれます。
リンタというのは、（ご存じだと思いますが）良くない書き方をされたコードに対して警告してくれるツールのことです。たとえば Python なら Ruff のようなツールにリンターが組み込まれています。お世話になっている方も多いでしょう。しかし Lean のリンターはおもしろいことに、Lean 自体を使って普通のプログラムと同じように実装することができます。
たとえば、Batteries というライブラリで定義されている docBlame リンタの定義はこうです。
仮に Lean 4 のコードが読めないとしても問題ありません。.lean ファイル内にしれっと定義されていることをお伝えしたいだけです。リンターというのは「コード自体」について推論することが必要ですが、Lean では「Lean のコード」を Lean のデータとして扱うことができるので、こういうことができるのかもしれません。コード自体をデータとして扱えるのは Lisp や Julia もそうだと聞いていますが、Lisp や Julia が真のマクロを持つように、Lean も真のマクロを持っています。
#lint コマンドは少なくともファイルごとにリンタを実行することが可能で、ファイルの末尾で使用すればそのファイルの内容についてリンタを実行してくれます。可能なリンタとして何が存在するのかは、#list_linters という別のコマンドを実行することで教えてもらうことができます。
コードについて
ここまでコード不在で話をしてきましたが、ZENN では Lean のコードの構文ハイライトは効かないようですし、お手軽に実行することもできません。私の書いている日本語 Lean ドキュメントである Lean by Example の該当ページへのリンクを貼っておきます。
Lean by Example では、右上にある再生ボタンのようなボタンを押すことでほぼすべてのページからオンラインプレイグラウンドに飛ぶことができ、環境構築不要で Lean コードが実行できるようになっています。
終わりに
Lean は詳しく学ぶ価値のあるプログラミング言語です。数学、形式証明、自動証明、関数型プログラミングなどのどれかに興味があれば、Lean から多くの学びを得ることができると思います。興味があればぜひご自分でも調べてみてください。
Discussion