関数適用は項とそれに続く1つ以上の引数、または0個以上の引数と最後の ellipsis から構成されます。
term ::= ... | term argument+ | term argument* ..
6.4. 関数適用（Function Application）
通常、関数適用は並置するように記述されます：引数は関数の後ろに置かれ、その間には少なくとも1つの空白が入ります。Lean の型理論では、すべての関数は正確に1つの引数を取り、正確に1つの値を生成します。すべての関数適用は1つの関数と1つの引数を組み合わせたものです。複数引数はカリー化で表現されます。
高レベルの項言語は、関数を1つ以上の引数と共に1つのユニットとして扱い、通常の位置引数と共に暗黙・オプショナル・名前によって指定される引数などの追加機能をサポートします。エラボレータはこれらをコア型理論の単純なモデルに変換します。
syntax
syntaxArguments
関数引数は項または 名前付き引数 （named argument）です。
argument ::= ... | term | ((ident | ident ):=term)
関数のコア言語型は、最終的にできた式における引数の配置を決定します。関数型には期待されるパラメータの名前が含まれます。Lean のコア言語において非依存関数型は、そのパラメータ名が本体に出現しないような依存関数型としてエンコードされます。さらに、この場合の名前は、名前付き引数の名前として書けないように内部的に選択されます；これは偶発的なキャプチャを防ぐために重要です。
関数が期待する各パラメータには名前があります。関数の引数の型を繰り返しながら、引数は以下のように引数の列から選択されます：
-
パラメータ名が名前付き引数の名前と一致する場合、その引数が選択されます。
-
パラメータが 暗黙 である場合、そのパラメータの型で新しいメタ変数が作成・選択されます。
-
パラメータが インスタンス暗黙 である場合、そのパラメータの型で新しいインスタンスのメタ変数が作成され、挿入されます。インスタンスのメタ変数は後で統合するようスケジュールされます。
-
パラメータが 厳密な暗黙 パラメータであり、まだ選択されていない名前付き引数または位置引数がある場合、そのパラメータの型で新しいメタ変数が作成・選択されます。
-
パラメータが明示的な場合、次の位置引数が選択され、エラボレートされます。位置引数が無い場合：
-
パラメータが optional parameter として宣言されている場合、そのデフォルト値が引数として選択されます。
-
パラメータが automatic parameter である場合、関連するタクティクスクリプトが引数を構築するために実行されます。
-
パラメータがオプショナルでも自動パラメータでもなく、ellipsis もない場合、引数として新しい変数が選択されます。ellipsis がある場合、引数が暗黙的であるかのように、新しいメタ変数が選択されます。
-
特殊なケースとして、 パターン の中で関数適用が発生し、ellipsis がある場合、オプショナル引数や自動引数は挿入されずに、ユニバーサルパターン（_）になります。
型が関数型でなく、引数が残っている場合はエラーとなります。すべての引数が挿入され、ellipsis がある場合、暗黙の引数であるかのように、欠落している引数にはすべて新しいメタ変数として設定されます。もし足りない明示的な位置変数のために新しい変数が作成された場合、適用全体はそれらを束縛する Lean.Parser.Term.fun : termfun 項でラップされます。最後に、インスタンス統合が呼び出され、可能な限り多くのメタ変数が解決されます：
-
関数適用全体に対して型が推論されます。このため、型推論中に発生する単一化により、いくつかのメタ変数が解決されることがあります。
-
インスタンスのメタ変数が統合されます。 デフォルトインスタンス は、推論された型がインスタンスの1つの出力パラメータであるメタ変数である場合にのみ使用されます。
-
期待される型がある場合、それは推論される型に単一化されます；しかし、この単一化の結果生じたエラーは破棄されます。期待される型と推論される型が等しい場合、単一化によって残された暗黙の引数のメタ変数を解決することができます。等しくない場合、周囲のエラボレータが coercions を挿入したり、 モナド持ち上げ ができる可能性があるため、エラーは投げられません。
名前付き引数
Lean.Parser.Command.check : command#check コマンドは、関数呼び出しのために挿入された引数を検査するために使用することができます。
関数 sum3 は3つの明示的な Nat パラメータを取り、名前は x・y・z です。
def sum3 (x y z : Nat) : Nat := x + y + z
この3つの引数はすべて、位置引数として提供することができます。
#check sum3 1 3 8
sum3 1 3 8 : Nat
また名前での提供も可能です。
#check sum3 (x := 1) (y := 3) (z := 8)
sum3 1 3 8 : Nat
引数を名前で指定する場合、順序は問いません。
#check sum3 (y := 3) (z := 8) (x := 1)
sum3 1 3 8 : Nat
名前付き引数と位置引数は自由に混在させることができます。
#check sum3 1 (z := 8) (y := 3)
sum3 1 3 8 : Nat
名前付き引数と位置引数は自由に混在させることができます。ある引数が名前で指定された場合、それが位置引数で使用される可能性があったとしてもその引数が使用されます。
#check sum3 1 (x := 8) (y := 3)
sum3 8 3 1 : Nat
ある名前付き引数が提供されていない引数の後に挿入される場合、提供された引数が記述された関数が作成されます。
#check sum3 (z := 8)
fun x y => sum3 x y 8 : Nat → Nat → Nat
裏側では、引数の名前は関数型に保存されます。つまり、残りの引数は再び名前で呼び出すことができます。
#check (sum3 (z := 8)) (y := 1)
fun x => (fun x y => sum3 x y 8) x 1 : Nat → Nat
オプショナルパラメータと自動パラメータは Lean のコア型理論の一部ではありません。これらは optParam ・ autoParam ガジェット を使ってエンコードされます。
def
optParam.{u} (α : Sort u) (default : α) : Sort u
def
autoParam.{u} (α : Sort u)
(tactic : Lean.Syntax) : Sort u
6.4.1. 一般化されたフィールド記法（Generalized Field Notation）
構造体フィールドの節 では、型が構造体である項からフィールドを射影するための記法を説明しています。一般的なフィールド記法は、空白で区切られていないドット（.）と識別子が続く項で構成されます。
syntaxField Notation
term ::= ...
| The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
More precisely,
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
`e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type,
the above is repeated for every base type of the structure.
The field index notation `e.i`, where `i` is a positive number,
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. 項の型が0個以上の引数に適用される定数である場合、項がフィールドを持つ構造体または型クラスのインスタンスであるかどうかに関わらず、 フィールド記法 （field notation）を使用して関数を適用することができます。フィールド記法を使用して他の関数を適用することを 一般化されたフィールド記法 （generalized field notation）と呼びます。
ドットに続く識別子は、その項の型の名前空間で検索されます。これはその定数の名前です。その型が定数の適用でない場合（関数・メタ変数・宇宙など）、名前空間はないため一般化されたフィールド記法は使用できません。フィールドが見つからなくても、定数を展開することで定数または定数の応用である型が得られる場合は、その新しい定数で処理を繰り返します。
関数が見つかると、ドットの前の項がその関数の引数になります。具体的には、その関数の型エラーとならない最初の明示的な引数になります。それを除けば、適用は通常通りにエラボレートされます。
一般化されたフィールド記法
型 Username は定数であるため、 Username 名前空間の関数は一般化されたフィールド記法を用いて Username 型を持つ項に適用することができます。
def Username := String
このような関数として Username.validate は、ユーザ名に先頭の空白文字が含まれていないこと、および許容される文字種のみが使用されていることをチェックします。その定義では、関数 String.isPrefixOf ・ String.any ・ Char.isAlpha ・ Char.isDigit の呼び出しで一般化されたフィールド記法が使用されています。 String.isPrefixOf では、2つの String 引数を取りますが、 " " はドットの前の項であるため、最初の引数として使用されます。Username.any は定義されておらず、 Username は String に展開されるため、 String.any は name が Username 型であるにも関わらず呼び出すことができます。
def Username.validate (name : Username) : Except String Unit := do
if " ".isPrefixOf name then
throw "Unexpected leading whitespace"
if name.any notOk then
throw "Unexpected character"
return ()
where
notOk (c : Char) : Bool :=
!c.isAlpha &&
!c.isDigit &&
!c ∈ ['_', ' ']
def root : Username := "root"
しかし、 Username.validate は String が Username に展開されないため、 "root" に対してフィールド記法を使って呼び出すことができません。
#eval "root".validate
invalid field 'validate', the environment does not contain 'String.validate' "root" has type String
#eval root.validate
Except.ok ()
option
pp.fieldNotation
Default value: true
(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied
syntaxControlling Field Notation
pp_nodot 属性は、関数を表示する際に Lean のプリティプリンタがフィールド記法を使わないようにします。
attr ::= ... | pp_nodot
フィールド記法の表示オフ
Nat.half はデフォルトでフィールド記法として表示されます。
def Nat.half : Nat → Nat
| 0 | 1 => 0
| n + 2 => n.half + 1
#check Nat.half Nat.zero
Nat.zero.half : Nat
pp_nodot に Nat.half を追加すると、項を表示する際に、フィールド記法の代わりに通常の関数適用構文が使用されるようになります。
attribute [pp_nodot] Nat.half
#check Nat.half Nat.zero
Nat.half Nat.zero : Nat
6.4.2. パイプライン構文（Pipeline Syntax）
パイプライン構文は、関数適用を記述する代替方法を提供します。繰り返されたパイプラインでは、入れ子になった括弧の代わりにパースの優先順位を使用して、位置引数への関数の適用を入れ子にします。
syntaxPipelines
右パイプ記法は、パイプの右側の項をその左側の項に適用します。
term ::= ...
| Haskell-like pipe operator `|>`. `x |> f` means the same as the same as `f x`,
and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
左パイプ記法は、パイプの左側の項をその右側の項に適用します。
term ::= ...
| Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`,
except that it parses `x` with lower precedence, which means that `f <| g <| x`
is interpreted as `f (g x)` rather than `(f g) x`.
右パイプライン記法の直観的な考え方は、左側の値が最初の関数に送られ、その結果が2番目の関数に送られるというものです。左パイプライン記法では、右側の値が左方向に与えられます。
右パイプライン記法
右パイプラインは、ある項に対して一連の関数を呼び出すために使用できます。コードを読む人に対して、変換されるデータが強調されやすくなります。
#eval "Hello!" |> String.toList |> List.reverse |> List.head!
'!'
左パイプライン記法
左パイプラインは、ある項に対して一連の関数を呼び出すために使用できます。データよりも関数が強調されやすくなります。
#eval List.head! <| List.reverse <| String.toList <| "Hello!"
'!'
syntaxPipeline Fields
パイプライン記法には 一般化されたフィールド記法 を用いているバージョンがあります。
term ::= ...
| `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
term ::= ...
| `e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.
e |>.f arg は (e).f arg の別の構文です。
パイプラインのフィールド
引数の順序が適切ではないため、パイプラインで使用するには不便な関数もあります。例えば、 Array.push は第1引数に Nat ではなく配列を取るため次のようなエラーが発生します：
#eval #[1, 2, 3] |> Array.push 4
failed to synthesize OfNat (Array ?m.4) 4 numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is Array ?m.4 due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.
パイプラインのフィールド記法を使うと、配列は型が正しい最初に位置に挿入されます：
#eval #[1, 2, 3] |>.push 4
#[1, 2, 3, 4]
このプロセスは繰り返すことができます：
#eval #[1, 2, 3] |>.push 4 |>.reverse |>.push 0 |>.reverse
#[0, 1, 2, 3, 4]