その他の便利な機能

パイプ演算子

関数は通常、引数の前に書かれます。これはプログラムを左から右に読む際に、関数の出力が最重要だという見方を助長します。つまり、関数は達成すべきゴール（つまり計算すべき値）を持っており、そのプロセスをサポートするために引数を受け取るという視点です。しかし、プログラムの中には出力の生成のために入力が逐次的に改良されていく、という観点のほうが理解しやすいものも存在します。このような状況に対して、LeanはF#にあるものと似た パイプライン 演算子を提供しています。パイプライン演算子はClojureのスレッディングマクロと同じ状況化で有用です。

パイプライン E1 |> E2 は E2 E1 の省略形です。例えば、以下を評価すると：

#eval some 5 |> toString

以下の結果になります：

"(some 5)"

このように強調箇所を変えることでより読みやすくなるプログラムもありますが、多くのコンポーネントを含む場合にパイプラインはその本領を発揮します。

以下の定義に対して：

def times3 (n : Nat) : Nat := n * 3

以下のパイプラインは：

#eval 5 |> times3 |> toString |> ("It is " ++ ·)

以下を出力します：

"It is 15"

より一般的には、パイプラインの列 E1 |> E2 |> E3 |> E4 は関数適用のネスト E4 (E3 (E2 E1)) の省略形です。

パイプラインは反対向きに書くこともできます。この場合、変換する対象のデータを先に持ってきません；しかし、入れ子になった括弧が多くて読者が困るような場合にはパイプラインによって適用のステップを明確にすることができます。先ほどの例は以下の記述と等価です：

#eval ("It is " ++ ·) <| toString <| times3 <| 5

これは以下の短縮形です：

#eval ("It is " ++ ·) (toString (times3 5))

Leanのメソッドのドット記法は、ドットの前の型名を使ってドットの後ろの演算子の名前空間を解決するもので、パイプラインと似た目的を提供しています。仮にパイプライン演算子が無くとも、[1, 2, 3].reverse の代わりに List.reverse [1, 2, 3] と書くことは可能です。しかし、パイプライン演算子はドットを付けた関数をたくさん使う場合でも便利です。([1, 2, 3].reverse.drop 1).reverse は [1, 2, 3] |> List.reverse |> List.drop 1 |> List.reverse と書くこともできます。この書き方では、ただ引数を受け取るという理由だけで式を括弧で囲む必要がなく、KotlinやC#のような言語での便利なメソッドチェーンを再現しています。ただし、この場合は名前空間を手動で指定する必要があります。そこで究極的な便利機能として、Leanは「パイプラインドット」演算子を提供しています。これは関数をパイプラインのようにグループ化しますが、名前空間を解決するために型名を使用します。「パイプラインドット」を使用すると、上記の例は [1, 2, 3] |>.reverse |>.drop 1 |>.reverse と書き換えることができます。

無限ループ

do ブロックの中で、repeat キーワードを使うと無限ループを作れます。例えば、"Spam!" という文字列を連投するプログラムで以下のように使われます：

def spam : IO Unit := do
  repeat IO.println "Spam!"

repeat ループは for ループと同じように break と continue をサポートしています。

feline の実装における dump 関数は再帰関数を使って永遠に実行していました：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

この関数は repeat を使うことで劇的に短縮できます：

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  repeat do
    let buf ← stream.read bufsize
    if buf.isEmpty then break
    stdout.write buf

spam も dump も、それ自体が無限再帰ではないため partial として宣言する必要はありません。その代わりに、repeat は ForM インスタンスが partial である型を使用します。関数の部分性は、関数の呼び出し時に「感染」することはありません。

whileループ

局所的な可変性を使ってプログラムを書く場合、while ループは if で break をガードするような repeat よりも便利です：

def dump (stream : IO.FS.Stream) : IO Unit := do
  let stdout ← IO.getStdout
  let mut buf ← stream.read bufsize
  while not buf.isEmpty do
    stdout.write buf
    buf ← stream.read bufsize

裏では、while は repeat をよりシンプルにした表記にすぎません。

Functional Programming in Lean 日本語訳

その他の便利な機能

パイプ演算子

無限ループ

whileループ