Lean日報: Lean のマクロは、Macro 型の項
はじめに
この Lean 日報ではシリーズ記事として、Lean について新たに学んだことを書いていきます。定期更新ではありません。
Lean とは何か
Lean は、プログラミング言語の一種です。しかしただの言語ではなくて、純粋関数型プログラミング言語かつ定理証明支援系でもあるという特徴を持ちます。数学の形式化や自動証明の構成、数学的問題について推論するAIの開発などに応用が期待されています。[1]
Macro 型
今回は Macro 型についてです。
Macro 型は、その名の通りマクロを表す型です。一般的なプログラミング言語の話として、マクロとは構文を構文に変換する操作のことです。[2] Lisp や Juila, Rust のどれかをご存じであればそれのマクロ機能を思い浮かべてもらえると良いと思います。Lean においても、マクロとは構文を構文に変換する操作であることに違いはありません。
しかしながら、Lean のマクロは Macro という型を持つ関数になっています。コード内のデータとして実現されているわけですね。具体的には、Syntax → MacroM Syntax という型を持つ関数です。実のところ Macro 型とは、Syntax → MacroM Syntax の省略形でしかありません。
Lean ではマクロを定義するのに便利な様々なコマンドがあります。
-
1 + 3の+記号のような演算子の類はnotationやinfixコマンドで定義できます。 - コマンドやタクティクに展開されるようなより一般的なマクロは
macroコマンドやmacro_rulesコマンドで定義できます。
こういったコマンドはすべて Macro 型のことなど気にせずに使うことができるものですが、実際には裏で Macro 型の項を生成していることを確かめることができます。whatsnew という、あるコマンドで生成された識別子を全部列挙することができるコマンドがあるので、それを使えばよいでしょう。
また逆に、多少手間がかかり冗長ではあるのですが、Macro 型の項が与えられればそこからマクロを定義することもできます。
このように、Lean のコード自体をあれこれするようなメタレベルの概念が、Lean 内のデータとして表現されているのも Lean のおもしろいところです。ここでは触れませんでしたが、Lean ではパーサも Lean 内のデータです。したがって、「あるコードが構文エラーになるかどうかのテスト」を普通の関数に対するテストと同じように書くことができたりします！
コードについて
ここまでコード不在で話をしてきましたが、ZENN では Lean のコードの構文ハイライトは効かないようですし、お手軽に実行することもできません。私の書いている日本語 Lean ドキュメントである Lean by Example の該当ページへのリンクを貼っておきます。
Lean by Example では、右上にある再生ボタンのようなボタンを押すことでほぼすべてのページからオンラインプレイグラウンドに飛ぶことができ、環境構築不要で Lean コードが実行できるようになっています。
終わりに
Lean は詳しく学ぶ価値のあるプログラミング言語です。数学、形式証明、自動証明、関数型プログラミングなどのどれかに興味があれば、Lean から多くの学びを得ることができると思います。興味があればぜひご自分でも調べてみてください。
Discussion