https://juliahimmel.de/blog/an-underappreciated-lean-feature/
この記事は、Lean のあまり知られていない名前解決機能 “dot notation respects open”、略して DNRO を紹介しています。これは、open された名前空間の中にある関数も、ドット記法の候補として探索する機能です。
問題：拡張関数が名前空間を汚染する
Lean では、
l.filter isEven
のようなドット記法を使えます。これは概ね、l : List α なら List.filter ... l のように、引数の型に対応する名前空間から関数を探す仕組みです。
この仕組みにより、既存の型に対して第三者が関数を追加できます。しかし、ライブラリ内部でしか使わない補助関数を、たとえば
String.prependChar
として定義すると、利用者の補完候補にも表示されます。実装詳細であるはずの関数が、正式な公開 API に見えてしまうという「名前空間汚染」が起きます。
private にする方法は単一ファイルなら有効ですが、複数ファイルから利用しにくくなります。内部用名前空間へ移すと、今度は便利なドット記法を失うように見えます。
DNROによる解決
補助関数を次のような完全名で定義します。
LeftPad.Internal.String.prependChar
そして実装側で、
open LeftPad.Internal
とすると、Lean は
s.prependChar c
を LeftPad.Internal.String.prependChar c s として解決できます。
一方、利用者が LeftPad.Internal を open しなければ、この関数は通常の String のドット補完には現れません。つまり、
- 実装内部ではドット記法を維持できる
- 公開される String 名前空間を汚染しない
- ファイル構成や private の制約にも縛られない
という利点があります。
一般的な設計パターン
DNROを使うと、他ライブラリの型に対する拡張を、
自分のライブラリ.相手の名前空間.関数名
という形で配置できます。たとえば、
MyLibrary.String.someFunction
MyLibrary.Std.someFunction
のような命名です。
さらに、通常の API と高度な API を分け、高度な関数だけを
open Library.Advanced
した場合にドット記法で利用可能にする、といった オプトイン型API も設計できます。Lean 本体でも、基本型や標準ライブラリの名前空間から内部用ヘルパーを追い出すため、この方式を利用していく方針だと説明されています。DNRO自体は2024年11月に追加され、Lean 4.15に含まれました。
副作用：open の曖昧性
この命名法を多用すると、別の問題が生じます。
namespace MyLibrary
open String
と書いた場合、当初はグローバルな root.String が開かれていても、後から MyLibrary.String が作られると、同じ open String がそちらを指すようになります。その結果、依存ライブラリの更新などによって、無関係に見えるコードが突然壊れる可能性があります。
Lean 4.33では、この状況を検出する 曖昧な open に対する新しいリンター が追加されました。修正方法は、たとえば次のいずれかです。
open root.String
または、周囲の namespace の外側で open String します。
要するに
この記事の主張は、Leanでは「既存型にドット記法で使える関数を追加すること」と「その型の公開名前空間を汚染しないこと」を両立できる、というものです。
DNROは小さな名前解決規則ですが、大規模ライブラリにおけるAPIの境界、内部実装の隠蔽、他ライブラリへの安全な拡張という点で、かなり重要な機能だと評価されています。
この記事は、Lean のあまり知られていない名前解決機能 “dot notation respects open”、略して DNRO を紹介しています。これは、open された名前空間の中にある関数も、ドット記法の候補として探索する機能です。
問題：拡張関数が名前空間を汚染する
Lean では、
l.filter isEven
のようなドット記法を使えます。これは概ね、l : List α なら List.filter ... l のように、引数の型に対応する名前空間から関数を探す仕組みです。
この仕組みにより、既存の型に対して第三者が関数を追加できます。しかし、ライブラリ内部でしか使わない補助関数を、たとえば
String.prependChar
として定義すると、利用者の補完候補にも表示されます。実装詳細であるはずの関数が、正式な公開 API に見えてしまうという「名前空間汚染」が起きます。
private にする方法は単一ファイルなら有効ですが、複数ファイルから利用しにくくなります。内部用名前空間へ移すと、今度は便利なドット記法を失うように見えます。
DNROによる解決
補助関数を次のような完全名で定義します。
LeftPad.Internal.String.prependChar
そして実装側で、
open LeftPad.Internal
とすると、Lean は
s.prependChar c
を LeftPad.Internal.String.prependChar c s として解決できます。
一方、利用者が LeftPad.Internal を open しなければ、この関数は通常の String のドット補完には現れません。つまり、
という利点があります。
一般的な設計パターン
DNROを使うと、他ライブラリの型に対する拡張を、
自分のライブラリ.相手の名前空間.関数名
という形で配置できます。たとえば、
MyLibrary.String.someFunction
MyLibrary.Std.someFunction
のような命名です。
さらに、通常の API と高度な API を分け、高度な関数だけを
open Library.Advanced
した場合にドット記法で利用可能にする、といった オプトイン型API も設計できます。Lean 本体でも、基本型や標準ライブラリの名前空間から内部用ヘルパーを追い出すため、この方式を利用していく方針だと説明されています。DNRO自体は2024年11月に追加され、Lean 4.15に含まれました。
副作用：open の曖昧性
この命名法を多用すると、別の問題が生じます。
namespace MyLibrary
open String
と書いた場合、当初はグローバルな root.String が開かれていても、後から MyLibrary.String が作られると、同じ open String がそちらを指すようになります。その結果、依存ライブラリの更新などによって、無関係に見えるコードが突然壊れる可能性があります。
Lean 4.33では、この状況を検出する 曖昧な open に対する新しいリンター が追加されました。修正方法は、たとえば次のいずれかです。
open root.String
または、周囲の namespace の外側で open String します。
要するに
この記事の主張は、Leanでは「既存型にドット記法で使える関数を追加すること」と「その型の公開名前空間を汚染しないこと」を両立できる、というものです。
DNROは小さな名前解決規則ですが、大規模ライブラリにおけるAPIの境界、内部実装の隠蔽、他ライブラリへの安全な拡張という点で、かなり重要な機能だと評価されています。