型
型は計算できる値に基づいてプログラムを分類します。型がプログラムの中で果たす役割は多岐に渡ります：
- 型により、コンパイラが値のメモリ内表現について判断できるようになります。
- 型は、プログラマが自分の意図を他者に伝えるのに役立ちます。また型は、関数の入力と出力に対する軽量な仕様として機能します。コンパイラはプログラムが実際にその仕様を満たすことを検証できます。
- 型は文字列に数字を足してしまうようなミスを未然に防ぎ、プログラムに必要なテストの数を減らすことができます。
- 型は Lean のコンパイラが補助コードを自動生成するのを助け、ボイラープレートを減らすことができます。
Lean の型システムは非常に表現力に富んでいます。型によって「このソート関数は入力の並べ替えを返す」というような強力な仕様や、「この関数は引数の値によって戻り値の型が異なる」というような柔軟な仕様をエンコードすることができます。型システムは、数学の定理を証明するための本格的な論理として使うこともできます。しかし、この最先端の表現力は、より単純な型の必要性を排除するものではありません。単純な型を理解することは、より高度な機能を使うための前提条件です。
Lean のすべてのプログラムは型を持たなければなりません。特に、すべての式は評価される前に型を持っていなければいけません。これまでの例では、Lean は自分で型を推測することができましたが、時には型を提供する必要があります。型の指定はコロン演算子を使って行います：
#eval (1 + 2 : Nat)
ここで Nat は自然数の型で、任意精度の符号なし整数です。Lean では、Nat は非負整数リテラルのデフォルト型です。このデフォルトの型は必ずしも最良の選択ではありません。C 言語では、符号なし整数は、引き算の結果が0未満になる場合、表現可能な最大の数までアンダーフローします。しかし Nat 型は任意の大きさの符号なし整数を表現できますから、アンダーフローすべき最大の数が存在しません。したがって、Nat の引き算は、そうでなければ答えが負になるはずのときに0を返します。例えば
#eval 1 - 2
は -1 ではなく 0 を返します。負の整数を表現できる型を使うには、型を直接指定します：
#eval (1 - 2 : Int)
この型では、結果は予想通り-1です。
式を評価せずに型を確かめるには、#eval の代わりに #check を使います。例えば
#check (1 - 2 : Int)
は、実際の引き算は実行せず、1 - 2 : Int を報告します。
プログラムに型が与えられない場合、#check も #eval もエラーを返します。例えば：
#check String.append "hello" [" ", "world"]
というコードは下記のエラーを出力します。
application type mismatch
String.append "hello" [" ", "world"]
argument
[" ", "world"]
has type
List String : Type
but is expected to have type
String : Type
String.append の第2引数は文字列であることが期待されていますが、代わりに文字列のリストが代入されているからです。