式の評価

Lean を学ぶプログラマが理解すべき最も重要なことは，評価の仕組みです．評価とは，算数で行うような式の値を求めるプロセスのことです．例えば，15-6 の値は 9，2×(3＋1) の値は 8 です．後者の式の値を求めるとき，まず 3＋1 が 4 に置き換えられて 2×4 となります．これは簡約して 8 にできます．数式に変数が含まれることがあります：x+1 の値は，x の値がわかるまで計算できません．Lean では，プログラムはまず第一に式であり，計算を考える第一の方法は，式を評価して値を求めることです．

ほとんどのプログラミング言語は命令型であり，プログラムは，プログラムの結果を求めるために実行されるべき一連の文で構成されています．プログラムは可変なメモリにアクセスできるので，変数が参照する値は時間とともに変化する可能性があります．可変な状態に加えて，プログラムには，ファイルの削除・ネットワーク接続の発信・例外のスローまたはキャッチ・データベースからのデータの読み込みなど，他の副作用があるかもしれません．「副作用」とは，本質的に，数学的な式を評価するモデルに従わないプログラム内で起こりうることの総称です．

しかし Lean では，プログラムは数式と同じように機能します．一度値が与えられた変数は，再代入できません．式を評価しても副作用はありません．2つの式が同じ値を持つ場合，一方を他方に置き換えても，プログラムが異なる結果を計算することはありません．これは，Lean を使ってコンソールに Hello, world！ と書くことができないという意味ではありません．しかし I/O の実行は Lean を扱う経験の核心部分ではないとは言えるでしょう．そこで，この章では Lean を使って対話的に式を評価する方法に焦点を当て，次の章で Hello, world！ プログラムの書き方，コンパイル方法，実行方法について説明します．

Lean に式の評価をしてもらいたいとき，エディタで式の前に #eval と書けば結果を報告してくれます．通常，カーソルやマウスポインタを #eval の上に置くと結果が表示されます．例えば，

#eval 1 + 2

と書くと 3 と表示されます．

Lean は通常の算術演算子の優先順位と結合法則に従います．つまり，

#eval 1 + 2 * 5

は 15 ではなく 11 を返します．

通常の数学的表記法でも，大半のプログラミング言語でも，関数をその引数に適用する際には括弧を使います（例：f(x)）が，Lean は単に関数をその引数の横に書きます (例：f x)．関数の使用は最も一般的な操作のひとつであるため，簡潔であることが重要なのです．"Hello, Lean!" を計算するには，

#eval String.append("Hello, ", "Lean!")

と書く代わりに，関数の2つの引数を単に空白区切りで隣に書いて

#eval String.append "Hello, " "Lean!"

とします．

算術の演算順序規則で，(1 + 2) * 5 という式に括弧が必要なように，関数の引数を別の関数呼び出しで計算する場合にも括弧が必要です．例えば次の式では括弧が必要です．

#eval String.append "great " (String.append "oak " "tree")

そうしないと，2番目の String.append は，"oak " と "tree " を引数として渡された関数としてではなく，最初の String.append の引数として解釈されてしまうからです．最初に String.append の内部呼び出しの値が評価され，その値を "great " に追加することで，最終的な値 "great oak tree " を得ることができます．

命令形言語には，しばしば2種類の条件分岐があります：Bool 値に基づいてどの命令を実行するかを決定する条件文と，Bool 値に基づいて2つの式のうちどちらを評価するかを決定する条件式です．たとえば C や C++ では，条件文は if と else を使って書かれ，条件式は三項演算子 ? : を使って書かれます．Python では，条件文は if で始まりますが，条件式は if を真ん中に置きます．Lean はというと式指向の関数型言語ですから，条件文はありません．条件式のみです．条件式は if，then，else を使って書かれます．例えば，

String.append "it is " (if 1 > 2 then "yes" else "no")

は次のように評価されます．

String.append "it is " (if false then "yes" else "no")

これはさらに次のように評価され，

String.append "it is " "no"

最終的に "it is no" と評価されます．

簡潔にするために，このような一連の評価ステップを矢印で区切って書くことがあります：

String.append "it is " (if 1 > 2 then "yes" else "no")
===>
String.append "it is " (if false then "yes" else "no")
===>
String.append "it is " "no"
===>
"it is no"

よくあるエラー

Lean に引数のない関数適用の評価を依頼すると，エラーメッセージが表示されます．たとえば，特に

#eval String.append "it is "

とすると，かなり長いエラーメッセージを出力します：

expression
  String.append "it is "
has type
  String → String
but instance
  Lean.MetaEval (String → String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

このメッセージは，一部の引数のみ与えられた Lean 関数が，残りの引数を待つ新しい関数を返すために発生します．Lean はユーザに関数を表示することができないため，表示するように要求されるとエラーを返すのです．

演習問題

次の式の値はなんでしょうか？答えを予想してから，Lean に入力してチェックしてみましょう．

  • 42 + 19
  • String.append "A" (String.append "B" "C")
  • String.append (String.append "A" "B") "C"
  • if 3 == 3 then 5 else 7
  • if 3 == 4 then "equal" else "not equal"