まとめ

式の評価

Leanでは、式が評価されるときに計算も行われます。これは数式の通常のルールに従って行われます：式全体が値になるまで、通常の演算順序に従って部分式が値で置き換えられます。if や match を評価する場合、条件の値やマッチの対象が見つかるまでは枝の中の式は評価されません。

一度値が与えられると、変数は決して変化しません。これは数学と似ている一方でほとんどのプログラミング言語と異なった性質です。Leanの変数は単に値のプレースホルダであり、新しい値を書き込むことができるアドレスではありません。変数の値は def によるグローバル定義、let によるローカル定義、関数への名前付き引数、パターンマッチによって得られます。

関数

Leanにおいて関数は第一級です。つまり、関数をほかの関数に引数として渡したり、変数に保存したり、ほかの値と同じように使用することができます。Leanのすべての関数は必ず1つの引数を取ります。2つ以上の引数を取る関数を実装する場合には、Leanはカリー化と呼ばれるテクニックを使います。これは複数引数のうち最初の引数を受け取ってそれ以降の引数を受け取るような関数を返すようにするものです。引数を取らない関数を実装する場合には、Leanでは Unit 型という引数として最低限の情報を持つ型を使用します。

関数の実装方法は主に以下の3つがあります：

1. fun を用いた無名関数。例として、Point のフィールドの交換を行う関数は fun (point : Point) => { x := point.y, y := point.x : Point } と書くことができます。

2. 括弧の中で一つ以上の中黒点を置いた非常にシンプルな無名関数。各中黒点は関数の引数になり、括弧は関数の本体の範囲を仕切ります。例として、引数から1を引く関数 fun x => x - 1 の代わりに (· - 1) とも書けます。

3. def か let に引数のリストかパターンマッチ記法を続けるようにして定義した関数。

型

Leanはすべての式が型を持っていることをチェックします。Leanでの型とは何かしらの式について最終的に見つかるかもしれない値を記述したもので、例えば Int や Potin 、{α : Type} → Nat → α → List α 、Option (String ⊕ (Nat × String)) のようなものになります。ほかの言語と同様に、Leanの型はLeanのコンパイラによってチェックされるプログラムのための軽量な仕様を表現することができ、一部の単体テストの必要性を排除します。ほとんどの言語とは異なり、Leanの型は任意の数学も表現でき、プログラミングと定理証明の世界を統合しています。Leanを定理証明に使うことは本書の範囲外ですが、 Theorem Proving in Lean 4 にてこのトピックに関する詳細な情報があります。¹

式の中には複数の型を指定できるものもあります。例えば、3 は Int にも Nat にもなります。Leanでは、これは同じものに対して2つの異なる型あるというよりも、一つは Nat 型でもう一つは Int 型である2つの別々の式がたまたま同じように書かれたと理解すべきです。

Leanは自動的に型を決定できることもありますが、多くの場合、型はユーザによって提供されなければなりません。これはLeanの型システムが非常に表現力豊かだからです。仮にLeanが型を見つけることが出来たとしても、それが期待した型ではない可能性があります。3 は Int として使用されることを意図しているかもしれませんが、一切制約がない場合、Leanは Nat という型を与えます。一般的に、ほとんどの型は明示的に記述し、非常に明白な型はLeanに埋めてもらうようにするとよいでしょう。これはLeanのエラーメッセージを改善し、プログラマの意図をより明確にするのに役立ちます。

関数やデータ型の中には、型を引数に取るものがあります。これは 多相性 （polymorphic）と呼ばれます。多相性によって、リストの要素がどの型を持っているかを気にせずにリストの長さを計算するようなプログラムが可能になります。型はLeanにおいて第一級であるため、多相性は特別な構文を必要とせず、型はほかの引数と同じように渡されます。関数型において型引数に名前を与えることで、後の型がその引数に言及できるようになり、その関数を引数に適用した型は引数の名前を引数の値に置き換えることで求められます。

構造体と帰納的型

Leanでは structure や inductive の機能を使って、全く新しいデータ型を導入することができます。これらの新しいデータ型はたとえ定義が同じであったとしても他のデータ型と同じであるとはみなされません。データ型はその値を構築する方法を説明する コンストラクタ （constructor）を持ち、各コンストラクタはいくつかの引数を取ります。Leanのコンストラクタはオブジェクト指向言語のコンストラクタとは異なります：Leanのコンストラクタは、割り当てられたオブジェクトを初期化するアクティブなコードではなく、データを保持する不活性なものです。

一般的に、sturucture は直積型（つまり、任意の数の引数を取るコンストラクタを1つだけ持つ型）を導入するために使用され、inductive は直和型（つまり、多数の異なるコンストラクタを持つ型）を導入するために使用されます。sturucture で定義されたデータ型はコンストラクタの引数ごとにアクセサ関数が提供されます。構造体と帰納的データ型のどちらもパターンマッチにかけることができます。パターンマッチはコンストラクタを呼び出すために使用される構文のサブセットを使用して、コンストラクタの内部に格納されている値を展開します。パターンマッチは、値の作成方法を知るにはその値を消費する方法を知る必要があることを意味します。

再帰

定義されている名前がその定義自体で使われている場合、定義は再帰的です。Leanはプログラミング言語であると同時に対話型定理証明器であるため、再帰的定義には一定の制限があります。Leanの論理的な側面では、循環的な定義は論理的な矛盾につながる可能性があります。

再帰的定義がLeanの論理的側面を損なわないようにするために、Leanは再帰関数がどのような引数で呼び出されたとしても、すべての再帰関数が終了することを証明できなければなりません。実用としては、これは①再帰的な呼び出しがすべて入力の構造的に小さい部分で実行され、常にその構造の基底のケースに向かって進むことを保証するか、②ユーザが関数が常に終了するという他の証拠を提供する必要があること、のどちらかを意味します。同様に、再帰的帰納型はその型を引数として 受け取る 関数を取るコンストラクタを持つことはできません。なぜならこれは終了しない関数の実装を可能にするからです。