🌿

[macro_inline] 属性で短絡評価にする

に公開
macro
lean
lean4
短絡評価
tech

はじめに

短絡評価とは何か

「与えられた引数を全て評価するまでもなく値がわかるときには、残りの引数を評価しない」という評価戦略のことを 短絡評価 といいます。短絡評価が実装されている典型的な例は、論理演算子 && や || です。（それぞれ Lean で and と or の意味）他にも、デフォルト値を使って Option に包まれた値をはがす関数 Option.getD も Lean では短絡評価です。

「それって遅延評価じゃないの？」と思われたかもしれませんが、短絡評価は遅延評価より限定的です。無限リストを短絡評価を使って定義することはできませんが、遅延評価を使えば定義できます。

Lean は正格評価なので、引数を関数本体より先に評価します。つまり関数 f に引数 a b c を適用した値 f a b c を評価する際には、a b c の値をそれぞれ評価してから、それを f に代入して評価しようとします。これは短絡評価と相性が悪いようですが、「評価前に関数をマクロ展開する」ことで短絡評価を実現しています。

短絡評価を実装する

著者は不勉強なもので、他のプログラミング言語で「短絡評価を実装する」ことがどの程度一般的なのか知らないのですが、Lean では特段の苦労なく実装することができます。それが標題の [macro_inline] という属性です。この属性を関数に付与するだけで、その関数は「まるでマクロであるかのように」展開され、引数の評価が遅延されます。

/-- `Bool.and` を真似て自作した関数 -/
def Bool.myAnd : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

-- 第二引数が評価されており、短絡評価になっていない
/--
info: hello
---
info: false
-/
#guard_msgs in
  #eval Bool.myAnd false (dbg_trace "hello"; true)

-- `[macro_inline]` 属性を付与する
attribute [macro_inline] Bool.myAnd

-- 短絡評価になった！！
/-- info: false -/
#guard_msgs in
  #eval Bool.myAnd false (dbg_trace "hello"; true)

より詳しくは Lean by Example の該当記事をご覧ください。

https://lean-ja.github.io/lean-by-example/Reference/Attribute/MacroInline.html

Discussion