暗黙の引数

暗黙の引数とは、def コマンドや theorem コマンド、variable コマンドなどが受け取る構文の一つで、関数や定理の引数をユーザが明示的に与えなくても、Lean が文脈を読んで推論してくれるようになります。波括弧 {} で囲んで、{x y : A} のように書きます。

典型的な使用例

たとえば、暗黙の引数を使わなかった場合にどうなるかを見てみましょう。次の関数 List.subs は型パラメータ α : Type を受け取っていますが、第二引数 xs : List α を見れば α : Type が何であるかは分かるので、List.subs を使用する際に毎回 α を指定するのは冗長だと考えられます。

/-- 与えられたリストの部分リストを全て返す(明示的引数バージョン) -/
def List.subs_exp (α : Type) (xs : List α) : List (List α) :=
  match xs with
  | [] => [[]]
  | x :: xs =>
    let xss := subs_exp α xs
    xss ++ xss.map (x :: ·)

-- 型引数 α を明示的に与えて書いた場合
#eval List.subs_exp Nat [1, 2]

-- ホールを使って推論させる場合
#eval List.subs_exp _ [1, 2]

-- 型引数を与えないと（当然ながら）エラーになってしまう
#check_failure List.subs_exp [1, 2]

引数 α を暗黙の引数として受け取るように変更すれば、Lean が α : Type の内容を推論してくれるようになり、α を省略できるようになります。

/-- 与えられたリストの部分リストを全て返す(暗黙引数バージョン) -/
def List.subs_imp {α : Type} (xs : List α) : List (List α) :=
  match xs with
  | [] => [[]]
  | x :: xs =>
    let xss := subs_imp xs
    xss ++ xss.map (x :: ·)

-- 型引数を省略できるようになった
#eval List.subs_imp [1, 2]

-- 型引数を位置引数として与えると、今度はエラーになる
#check_failure List.subs_imp Nat [1, 2]

明示的引数モード

暗黙の引数を受け取るものとして定義された関数や定理に対して、@ 記号を先頭に付けると全ての暗黙の引数の自動挿入が行われなくなります。つまり、すべての引数を手動で与える必要が生じます。

-- 2 つの暗黙引数を持つ関数
def List.map' {α β : Type} (f : α → β) : List α → List β
  | [] => []
  | x :: xs => f x :: map' f xs

-- 普通は次のように使う
#check List.map' (fun x => x == 1) [1, 2, 3]

-- `@` 記号を付けると手動で型引数を与えないといけなくなる
#check @List.map' Nat Bool (fun x => x == 1) [1, 2, 3]

少し、というかかなり細かい注意ですが、@ を付けても「暗黙引数が明示的引数に変わる」わけではありません。その証拠に、#check コマンドの出力を見ると暗黙引数のままになっています。

/- info: id.{u} {α : Sort u} (a : α) : α -/
#check id

-- `α` のバインダーが波括弧のままになっている
/- info: @id : {α : Sort u_1} → α → α -/
#check @id

構文的な性質

Lean.Parser.Term.implicitBinder というパーサが暗黙引数の構文に対応しており、このパーサのドキュメントコメントに次のように書かれている通り、構文としては暗黙の引数に型を指定しないことも許されます。

Implicit binder, like {x y : A} or {x y}. In regular applications, whenever all parameters before it have been specified, then a _ placeholder is automatically inserted for this parameter. Implicit parameters should be able to be determined from the other arguments and the return type by unification.

In @ explicit mode, implicit binders behave like explicit binders.

-- `x : α` と書いたので、`α` が何かの型であることは分かる
def myId {α} (x : α) := x