その他の便利な機能

Leanにはプログラムをより簡潔にする便利な機能がたくさんあります。

自動的な暗黙引数

Leanで多相関数を書く場合、基本的にすべての暗黙引数を列挙する必要はありません。その代わりに、単にそれらを参照するだけでよいのです。Leanが引数に現れなかった変数の型を決定できる場合、それらは自動的に暗黙の引数として挿入されます。例えば、先ほどの length の定義について：

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

{α : Type} を書かずに定義できます：

def length (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

これにより、多くの暗黙引数をとるような高度に多相的な定義を大幅に簡略化することができます。

パターンマッチによる定義

def で関数を定義するとき、引数に名前をつけてもすぐにパターンマッチに適用してしまうケースはよくあります。例えば、length では引数 xs は match でのみ使用されます。このような状況では、引数に名前を付けずに match 式のケースを直接書くことができます。

最初のステップは、引数の型をコロンの右側に移動させることです。例えば length の型は List α → Nat となります。次に、:= をパターンマッチの各ケースで置き換えます：

def length : List α → Nat
  | [] => 0
  | y :: ys => Nat.succ (length ys)

この構文は複数の引数を取る関数を定義するのにも使えます。この場合、パターンはカンマで区切られます。例えば、drop は整数値 $ n $ とリストを受け取り、先頭から $ n $ 個の要素を取り除いたリストを返します。

def drop : Nat → List α → List α
  | Nat.zero, xs => xs
  | _, [] => []
  | Nat.succ n, x :: xs => drop n xs

名前の付いた引数とパターンを同じ定義で使用することもできます。例えば、デフォルト値とオプション値を受け取り、オプション値が none の場合はデフォルト値を返す関数を書くことができます：

def fromOption (default : α) : Option α → α
  | none => default
  | some x => x

この関数は標準ライブラリに Option.getD という名前で定義されており、ドット記法で呼び出すことができます：

#eval (some "salmonberry").getD ""

"salmonberry"

#eval none.getD ""

""

計算の途中のステップに名前を付けると便利なことが多いものです。多くの場合、こうした中間値はそれだけで有用な概念を表しており、明示的に名前をつけることでプログラムを読みやすくすることができます。また中間値が複数回使われる場合もあります。ほかの多くの言語と同じように、Leanにて同じコードを2回書くと2回計算されることになる一方で、結果を変数に保存すると計算結果が保存されて再利用されることになります。

例えば、unzip はペアからなるリストをリストのペアに変換する関数です。ペアのリストが空の場合、unzip の結果は空のリストのペアになります。ペアのリストの先頭にペアがある場合、そのペアの2つのフィールドが残りのリストを unzip した結果に追加されます。この unzip の定義を完全に起こすと以下のようになります：

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    (x :: (unzip xys).fst, y :: (unzip xys).snd)

残念ながら、このコードには問題があります: これは必要以上に遅いのです。ペアのリストの各要素が2回の再帰呼び出しを行うため、この関数には指数関数的な時間がかかります。しかし、どちらの再帰呼び出しも結果は同じであるため、再帰呼び出しを2回行う必要はありません。

Leanでは再帰呼び出しの結果を let を使って名前を付け、保存することができます。let によるローカル定義は def によるトップレベル定義と似ています：この構文ではローカル定義する名前、必要であれば引数、型シグネチャ、そして := に続く本体を取ります。ローカル定義の後、この定義が使用可能な式（ let 式の本体（body）と呼ばれます）は次の行からかつ let キーワードが定義された列と同じかそれよりも後ろから始まる必要があります。例えば let は unzip で次のように使用することができます：

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped : List α × List β := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

let を1行で使用するには、ローカル定義と本体をセミコロンで区切ります。

let を使用したローカル定義では、1つのパターンでデータ型のすべてのケースにマッチする場合であればパターンマッチを使うこともできます。unzip の場合、再帰呼び出しの結果はペアになります。ペアは単一のコンストラクタしか持たないので、unzipped という名前をペアのパターンに置き換えることができます：

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let (xs, ys) : List α × List β := unzip xys
    (x :: xs, y :: ys)

let を使ったパターンをうまく使えば、手作業でアクセサの呼び出しを書くよりもコードを読みやすくすることができます。

let と def の最大の違いは再帰的な let 定義は let rec と書いて明示的に示さなければならない点です。例えば、リストを反転させる方法の1つに、以下の定義のような再帰的な補助関数を用いるものがあります：

def reverse (xs : List α) : List α :=
  let rec helper : List α → List α → List α
    | [], soFar => soFar
    | y :: ys, soFar => helper ys (y :: soFar)
  helper xs []

補助関数は入力リストを下向きに進み、そのたびに1つの要素を soFar に移動していきます。入力リストの最後に到達すると、soFar には入力されたリストの逆順が格納されます。

型推論

多くの場合、Leanは式の型を自動的に決定することができます。このような場合、（ def による）トップレベルの定義と（ let による）ローカル定義のどちらでも明示的な型の省略ができます。例えば、再帰的に呼び出される unzip には注釈は不要です：

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

経験則として、（文字列や数値のような）リテラル値の型を省略することは通常うまくいきますが、Leanはリテラルの数値に対して意図した型よりも特殊な型を選ぶことがあります。Leanは関数適用の型を決定することができます、というのもすでに引数の型と戻り値の型を知っているからです。関数の定義で戻り値の型を省略することはよくありますが、引数には通常注釈が必要です。先ほどの unzipped のような関数ではない定義においては、その本体が型注釈を必要とせず、かつ定義の本体が関数適用である場合は型注釈を必要としません。

明示的な match 式を使用する場合、unzip の戻り値の型を省略することができます：

def unzip (pairs : List (α × β)) :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

一般論として、型注釈は少なすぎるよりは多すぎる方が良いです。まず、明示的な型は読み手にコードの前提を伝えます。たとえLeanによって型が決定できるものでも、Leanに型情報をいちいち問い合わせることなくコードを読むことができます。第二に、明示的な型はエラーの特定に役立ちます。プログラムが型について明示的であればあるほど、エラーメッセージはより有益なものになります。これはLeanに限らず非常に表現力豊かな型システムを持つ言語では特に重要です。第三に、型が明示されていることによって、そもそもプログラムを書くのが簡単になります。型は仕様であり、コンパイラのフィードバックは仕様を満たすプログラムを書くのに役立つツールになります。最後に、Leanの型推論はベストエフォートなシステムです。Leanの型システムは非常に表現力が豊かであるため、すべての式に対して「最良」な型や最も一般的な型を見つけることができません。つまり、型が得られたとしても、それが与えられたアプリケーションにとって「正しい」型であるという保証はないということです。例えば、14 は Nat にも Int にもなり得ます：

#check 14

14 : Nat

#check (14 : Int)

14 : Int

型注釈が欠落すると、エラーメッセージがわかりづらくなります。unzip の定義からすべての型を省略すると：

def unzip pairs :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

match 式について以下のようなメッセージが出力されます：

invalid match-expression, pattern contains metavariables
  []

これは match が受け取った検査対象の値の型を知る必要がありますが、その型が利用できなかったためです。「metavariable（メタ変数）」とはプログラムの未知の部分のことで、エラーメッセージでは ?m.XYZ と書かれます。これについては「多相性」節で解説しています。このプログラムでは、引数の型注釈が必要です。

非常に単純なプログラムであっても、型注釈を必要とするものがあります。例えば、恒等関数は渡された引数をそのまま返すだけの関数です。引数と型注釈を使うと次のようになります：

def id (x : α) : α := x

Leanはこの戻り値の型を自力で決定できます：

def id (x : α) := x

ここで引数の型を削除すると、以下のエラーを引き起こします：

def id x := x

failed to infer binder type

一般的に、「failed to infer（推論に失敗）」のようなメッセージやメタ変数に言及したメッセージは型注釈が足りていないというサインであることが多いです。特にLeanを学習している段階においては、ほとんどの型を明示的に提供することが有用です。

一斉パターンマッチ

パターンマッチング式は、パターンマッチング定義と同様に、一度に複数の値にマッチすることができます。検査する式とマッチするパターンは、定義に使われる構文と同じようにカンマで区切って記述します。以下は一斉パターンマッチを使用するバージョンの drop です：

def drop (n : Nat) (xs : List α) : List α :=
  match n, xs with
  | Nat.zero, ys => ys
  | _, [] => []
  | Nat.succ n , y :: ys => drop n ys

整数のパターンマッチ

「データ型・パターン・再帰」の節において、even は次のように定義されていました：

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

リストのパターンマッチを List.cons や List.nil を使うよりも読みやすくするための特別な構文があるように、自然数もリテラル数値と + を使ってマッチさせることができます。例えば、even は以下のように定義することもできます：

def even : Nat → Bool
  | 0 => true
  | n + 1 => not (even n)

この記法では、+ パターンの引数は異なる役割を果たします。裏側では、左の引数（上の n ）は何かしらの数値の Nat.succ パターンの引数になり、右の引数（上の 1 ）はパターンにラップする Nat.succ の数を決定します。さて、次に halve 関数の明示的なパターンでは Nat を2で割って余りを落とします：

def halve : Nat → Nat
  | Nat.zero => 0
  | Nat.succ Nat.zero => 0
  | Nat.succ (Nat.succ n) => halve n + 1

このパターンマッチは数値リテラルと + で置き換えることができます：

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | n + 2 => halve n + 1

この裏側では、上記二つの定義はどちらも完全に等価です。ここで覚えておいてほしいこととして、halve n + 1 は (halve n) + 1 と等価であり、halve (n + 1) とは等価ではありません。

この構文を使う場合、+ の第二引数は常に Nat のリテラルでなければなりません。また加算は可換であるにもかかわらず、パターン内の引数を反転させると次のようなエラーになることがあります：

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | 2 + n => halve n + 1

invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 2 n)

この制限により、Leanはパターン内で + 表記を使用する場合はすべて、その基礎となる Nat.succ 表記に変換することができます。

無名関数

Leanの関数はトップレベルで定義する必要はありません。式としての関数は fun 構文で生成されます。関数式はキーワード fun で始まり、1つ以上の引数が続き、その後に => を挟んで返される式が続きます。例えば、ある数値に1を足す関数は次のように書くことができます：

#check fun x => x + 1

fun x => x + 1 : Nat → Nat

型注釈は def と同じように括弧とコロンを使って記述します：

#check fun (x : Int) => x + 1

fun x => x + 1 : Int → Int

同じように、暗黙引数は波括弧を使って記述します：

#check fun {α : Type} (x : α) => x

fun {α} x => x : {α : Type} → α → α

この無名関数式のスタイルはしばしば ラムダ式 （lambda expression）と呼ばれます、というのもLeanではキーワード fun に対応するプログラミング言語の数学的な記述で使われる典型的な表記法はギリシャ文字のλ（ラムダ）だからです。Leanでも fun の代わりに λ を使うことができますが、fun と書く方が一般的です。

無名関数は def で使われる複数パターンのスタイルもサポートしています。例えば、ある自然数に対して、もし存在するならそのひとつ前を返す関数は以下のように書けます：

#check fun
  | 0 => none
  | n + 1 => some n

fun x =>
  match x with
  | 0 => none
  | Nat.succ n => some n : Nat → Option Nat

この関数に対してLeanから実際に付けられる情報には、名前付き引数と match 式があることに注意してください。Leanの便利な構文の短縮形の多くは、裏ではより単純な構文に拡張されており、抽象化が漏れることもあります。

def を使った定義で引数を取るものは、関数式に置き換えることができます。例えば、引数を2倍にする関数は以下のように書けます：

def double : Nat → Nat := fun
  | 0 => 0
  | k + 1 => double k + 2

無名関数が、fun x => x + 1 のように非常に単純な場合、関数を作成する構文はかなり冗長になります。この例では、6つの非空白文字が関数の導入に使用され、本体は3つの非空白文字で構成されています。このような単純なケースのために、Leanは省略記法を用意しています。括弧で囲まれた式の中で、中黒点 · が引数を表し、括弧の中の式が関数の本体になります。この関数は (· + 1) と書くこともできます。

中黒点は常に最も近い括弧から関数を生成します。例えば、(· + 5, 3) は数字のペアを返す関数で、((· + 5), 3) は関数と数字のペアです。複数の点が使用された場合、それらは左から右の順に複数の引数になります：

(· , ·) 1 2
===>
(1, ·) 2
===>
(1, 2)

無名関数は def や let で定義された関数とまったく同じように適用することができます。コマンド #eval (fun x => x + x) 5 の結果は以下のようになります：

一方で #eval (· * 2) 5 の結果は以下のようになります：

名前空間

Leanの各名前は名前の集まりである 名前空間 （namespace）の中に存在します。名前は . を使って名前空間に配置されるので、List.map は List 名前空間の map という名前になります。名前空間が異なる名前同士は、たとえ同じ名前であっても衝突することはありません。つまり、List.map と Array.map は異なる名前です。名前空間は入れ子にすることができるので、Project.Frontend.User.loginTime は入れ子の名前空間 Project.Frontend.User 内の loginTime という名前になります。

名前は名前空間内で直接定義することができます。例えば、double という名前は Nat 名前空間で定義することができます：

def Nat.double (x : Nat) : Nat := x + x

Nat は型の名前でもあるので、ドット記法を使えば Nat 型の式で Nat.double を呼び出すことができる：

#eval (4 : Nat).double

名前空間内で直接名前を定義するだけでなく、namespace コマンドと end コマンドを使用して一連の宣言を名前空間内に配置することができます。例えば、以下では名前空間 NewNamespace に triple と quadruple を定義しています：

namespace NewNamespace
def triple (x : Nat) : Nat := 3 * x
def quadruple (x : Nat) : Nat := 2 * x + 2 * x
end NewNamespace

これらを参照するには、それらの名前に接頭辞 NewNamespace. を付けます：

#check NewNamespace.triple

NewNamespace.triple (x : Nat) : Nat

#check NewNamespace.quadruple

NewNamespace.quadruple (x : Nat) : Nat

名前空間は開く（open）ことができます。これによって名前空間内の名前を明示的に指定することなく使うことができるようになります。式の前に open MyNamespace in と書くと、その式で MyNamespace の内容が使用できるようになります。以下の例で、timesTwelve は NewNamespace を開いた後に quadruple と triple の両方を使用しています：

def timesTwelve (x : Nat) :=
  open NewNamespace in
  quadruple (triple x)

名前空間はコマンドの前に開くこともできます。これにより単一の式内ではなく、コマンドのすべての部分で名前空間の内容を参照できるようになります。これを行うには、コマンドの前に open ... in を置きます：

open NewNamespace in
#check quadruple

NewNamespace.quadruple (x : Nat) : Nat

関数のシグネチャは、名前の完全な名前空間を示します。名前空間はさらに、ファイルの残りの部分 すべて のコマンドのために開くこともできます。これを行うには open のトップレベルの使用法から in を省略するだけです。

if let

直和型を持つ値を計算する場合、複数のコンストラクタの中のどれか一つだけが注目されることがよくあります。例えば、Markdownのインライン要素のサブセットを表す以下の型を考えます：

inductive Inline : Type where
  | lineBreak
  | string : String → Inline
  | emph : Inline → Inline
  | strong : Inline → Inline

ここで文字列要素を認識してその内容を抽出する関数を書くことができます：

def Inline.string? (inline : Inline) : Option String :=
  match inline with
  | Inline.string s => some s
  | _ => none

この関数の本体部分は、if を let と一緒に使うことでも記述できます：

def Inline.string? (inline : Inline) : Option String :=
  if let Inline.string s := inline then
    some s
  else none

これはパターンマッチの let 構文によく似ています。違いは、else の場合にフォールバックするようになるため、直和型で使用できる点です。文脈によっては、match の代わりに if let を使うとコードが読みやすくなることがあります。

構造体の位置引数

「構造体」の節では構造体の構築の仕方について2つの方法を紹介しました：

Point.mk 1 2 のようにコンストラクタを直接呼ぶ。

{ x := 1, y := 2 } のように括弧記法を使う。

文脈によっては、コンストラクタに直接名前を付けずに、名前ではなく位置で引数を渡すと便利な場合があります。例えば、様々な似たような構造体タイプを定義することで、ドメイン概念を分離しておくことができますが、コードを読む際にはそれらを実質的にタプルとして扱う方が自然です。このような文脈では、引数を角括弧 ⟨ と ⟩ で囲むことができます。Point は ⟨1, 2⟩ と書くことができます。ここで注意点です！この括弧は小なり記号 < と大なり記号 > のように見えますが、これらの括弧は違うものです。それぞれ \< と \> で入力できます。

名前付きコンストラクタ引数の波括弧表記と同様に、この位置指定構文は、型注釈やプログラム内の他の型情報から、Leanが構造体の型を決定できるコンテキストでのみ使用できます。例えば、#eval ⟨1, 2⟩ は以下のエラーを返します：

invalid constructor ⟨...⟩, expected type must be an inductive type 
  ?m.34991

エラーのメタ変数は、利用可能な型情報が無いためです。例えば、#eval (⟨1, 2⟩ : Point) のような注釈を追加することで問題は解決します：

{ x := 1.000000, y := 2.000000 }

文字列への内挿

Leanでは、文字列の先頭に s! を付けると内挿が発動し、文字列内の波括弧に含まれる式がその値に置き換えられます。これはPythonの f 文字列や、C#の $ 接頭辞付き文字列に似ています。例えば、

#eval s!"three fives is {NewNamespace.triple 5}"

は以下を出力します

"three fives is 15"

すべての式を文字列に内挿できるわけではありません。例えば、関数を内挿しようとするとエラーになります。

#check s!"three fives is {NewNamespace.triple}"

上記は以下を出力します

failed to synthesize instance
  ToString (Nat → Nat)

これは、関数を文字列に変換する標準的な方法がないからです。Leanコンパイラはさまざまな型の値を文字列に変換する方法を記述したテーブルを保持しており、failed to synthesize instance というメッセージはLeanコンパイラがこのテーブルの中から指定された型の要素を見つけられなかったことを意味します。これは「構造体」の節で説明した deriving Repr 構文と同じ言語機能を使用しています。

Functional Programming in Lean 日本語訳