依存型プログラミングの落とし穴

依存型の柔軟性によって、より便利なプログラムが型チェッカに受理されるようになります。というのも、この型の言語は表現力の乏しい型システムでは記述できないようなものについて記述するのに十分な表現力を備えているからです。同時に、依存型は非常にきめ細やかな仕様を表現できるため、バグを含むプログラムについて通常の型システムよりも多くのものが型チェッカで拒否されるようになります。このパワーには代償が伴います。

Row のような型を返す関数の内部と、その関数が生成する型との間の密結合などはより大きな困難の一例です：関数のインタフェースと実装の区別は関数が型の中で使われると崩れ始めます。通常、関数の型シグネチャや入出力の動作を変更しない限り、すべてのリファクタリングが有効です。クライアントコードを壊すことなく、関数はより効率的なアルゴリズムやデータ構造を使用するように書き換え、バグを修正し、ソースコードの明瞭性を向上させることができます。しかし、関数が型の中で使用されると、関数の実装内部は型の一部となり、したがって他のプログラムへの インタフェース の一部となります。

例として、以下の2つの Nat の加算の実装を見てみましょう。Nat.plusL は最初の引数に対して再帰的です：

def Nat.plusL : Nat → Nat → Nat
  | 0, k => k
  | n + 1, k => plusL n k + 1

一方、Nat.plusR は第2引数に対して再帰的です：

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

足し算の実装はどちらもベースの数学的なコンセプトに忠実であるため、同じ引数が与えられた時に同じ結果を返します。

しかし、これら2つの実装は型の中で用いられると全く異なるインタフェースを示します。例として、2つの Vect を連結する関数を考えてみましょう。この関数は引数の長さの和を長さとした Vect を返す必要があります。Vect は基本的に List により情報をもった型を加えたものであるので、この関数を List.append と同じように最初の引数に対してパターンマッチと再帰を行うように記述することは理にかなっているでしょう。型シグネチャとプレースホルダを指す最初のパターンマッチから始めると、2つのメッセージが得られます。

def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
  | .nil, ys => _
  | .cons x xs, ys => _

nil のケースにある最初のメッセージは、プレースホルダが plusL 0 k の長さを持つ Vect で置き換えられるべきであるということを述べています：

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
ys : Vect α k
⊢ Vect α (Nat.plusL 0 k)

cons のケースにある2番目のメッセージでは、プレースホルダは長さ plusL (n✝ + 1) k の Vect で置き換えられるべきであることを述べています：

don't know how to synthesize placeholder
context:
α : Type u_1
n k n✝ : Nat
x : α
xs : Vect α n✝
ys : Vect α k
⊢ Vect α (Nat.plusL (n✝ + 1) k)

n の後にある ダガー と呼ばれる記号はLeanが内部的に考案した名前を示すために使用されます。コンストラクタ cons の添字は n + 1 であり Vect の後続のリストの長さが n であることから、裏では最初の Vect に対して暗黙的に行われたパターンマッチによって、最初の Nat の値が絞り込まれます。ここで、n✝ は引数 n より1つ小さい Nat を表します。

Definitional Equality

plusL の定義には 0, k => k のパターンのケースがあります。これは最初のプレースホルダで使用されている長さに適用されるため、アンダースコアの型 Vect α (Nat.plusL 0 k) は Vect α k と別の書き方ができます。同様に、plusL は n + 1, k => plusN n k + 1 というパターンのケースを含んでいます。つまり、2つ目のアンダースコアの型は Vect α (plusL n✝ k + 1) と書くことと等価です。

裏で何が行われているかを明らかにするために、まず最初に Nat の引数を明示的に記述します。これによってプログラム中で今や名前が明示的に書かれることになるため、ダガーのないエラーメッセージが得られます：

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => _
  | n + 1, k, .cons x xs, ys => _

don't know how to synthesize placeholder
context:
α : Type u_1
k : Nat
ys : Vect α k
⊢ Vect α (Nat.plusL 0 k)

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL (n + 1) k)

アンダースコアに簡略化された型の注釈を付けても型エラーは発生しません。これはプログラム内で書かれた型がLeanが自力で見つけたものと等価であることを意味します：

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => (_ : Vect α k)
  | n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))

don't know how to synthesize placeholder
context:
α : Type u_1
k : Nat
ys : Vect α k
⊢ Vect α k

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL n k + 1)

最初のケースは Vect α k を要求し、ys はその型を持ちます。これは空リストを他のリストに追加するとそのリストが返されることと対になっています。最初のアンダースコアの代わりに ys を使って型を絞り込むと、プログラム中にまだ埋められていないアンダースコアは残り1つとなります：

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => ys
  | n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL n k + 1)

ここで非常に重要なことが起こりました。Leanが Vect α (Nat.plusL 0 k) を期待したコンテキストで Vect α k を受け取ったのです。しかし、Nat.plusL は abbrev ではないため、型チェック中に実行されるべくもないと思われるかもしれません。つまり何か別のことが起こっています。

何が起こっているかを理解する鍵となるのは、Leanが型チェックをする際に行うことはただ abbrev を展開するだけではないということです。それだけでなく、片方の型の任意の式がもう片方の型を期待するコンテキストで使われているような2つの型が等しいかどうかのチェックをしながら計算を行うこともできます。この性質は definitional equality と呼ばれ、とらえがたいものです。

当たり前ですが、同じように書かれた2つの型は definitionally equal です。例えば、Nat は Nat と、List String は List String と等しいと見なされるべきです。異なるデータ型から構築された任意の2つの具体的な型は等しくありません。そのため List Nat は Int と等しくありません。さらに、内部的な名前の変更だけが異なる型は等しいです。そのため、(n : Nat) → Vect String n は (k : Nat) → Vect String k と同じです。型は通常のデータを含むことができるため、definitional equality はデータが等しい場合についても記述しなければなりません。同じコンストラクタの使用は等しいです。そのため、0 は 0 と、[5, 3, 1] は [5, 3, 1] と等しくなります。

しかし、型に含まれるのは型に含まれるのは関数の矢印、データ型、コンストラクタだけではありません。型には 変数 と 関数 も含まれます。変数の definitional equality は比較的シンプルです：各変数は自分自身と等しくなります。そのため (n k : Nat) → Vect Int n は (n k : Nat) → Vect Int k と definitionally equal ではありません。一方で関数はもっと複雑です。数学では2つの関数が入力と出力の挙動が同じであるときに等しいと見なしますが、それをチェックする効率的なアルゴリズムは無いため、Leanでは definitionally equal なボディを持つ fun 式を持つ関数は definitionally equal であると見なします。言い換えると、2つの関数が definitionally equal であるためには 同じアルゴリズム を使い、同じ補助関数 を呼ばなければなりません。これは通常あまり役に立たないため、関数の definitional equality は2つの型に全く同じ定義関数が存在する場合に使用されることがほとんどです。

関数が型の中で 呼ばれた 場合、definitional equality のチェックによって関数呼び出しの簡約が発火される場合があります。型 Vect String (1 + 4) は、1 + 4 が 3 + 2 と definitionally equal であるため、型 Vect String (3 + 2) と definitionally equal です。これらの等価性をチェックするには、どちらも 5 に簡約され、コンストラクタのルールが5回使われることで確認できます。データに適用された関数の definitional equality は、まずそれらがすでに同じであるかのチェックを行います。つまるところ、["a", "b"] ++ ["c"] が ["a", "b"] ++ ["c"] と等しいことのチェックのために簡約する必要はないわけです。等しくなかった場合、関数が呼ばれ、得られた値で置き換えられ、その値がチェックされます。

全ての関数の引数が具体的なデータというわけではありません。例えば、型の中には zero と succ コンストラクタのどちらからも生成されていない Nat が含まれることがあります。型 (n : Nat) → Vect String n の中で、変数 n は Nat ですが、この関数が呼ばれるまではこれが どっちの Nat であるか知ることは不可能です。実際、この関数はまず 0 で呼び、その後で 17 を、それから 33 で呼び出されるかもしれません。appendL の定義で見たように、Nat 型の変数も plusL のような関数に渡すことができます。実際、型 (n : Nat) → Vect String n は (n : Nat) → Vect String (Nat.plusL 0 n) と definitionally equal となります。

n と Nat.plusL 0 n が definitionally equal である理由は、plusL のパターンマッチがその 最初の 引数を調べるからです。これは問題です：0は足し算の左右どちらともの単位元であるべきであるにもかかわらず、(n : Nat) → Vect String n は (n : Nat) → Vect String (Nat.plusL n 0) と definitionally equal ではない からです。これはパターンマッチが変数に遭遇したことで行き詰ってしまうことで発生します。n の実際の値がわかるまで、Nat.plusL n 0 のどのケースを選択すべきか知るすべはありません。

同じ問題がクエリの例での Row 関数でも発生します。Row の定義が中身が1つのリストと最低でも2つ以上要素を持つリストを分けているため、型 Row (c :: cs) はどのデータ型にも簡約することができません。つまり、具体的な List コンストラクタに対して変数 cs をマッチさせようとすると詰まってしまいます。これが Row を分解したり構成したりするほとんどすべての関数が Row の3つのケースと同じようにマッチさせる必要がある理由です：これを解消すると、パターンマッチにもコンストラクタにも使える具体的な型が見えてきます。

appendL の欠落しているケースでは Vect α (Nat.plusL n k + 1) が必要になります。この添字での + 1 によって次のステップで Vect.cons を使うことが示唆されます：

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => ys
  | n + 1, k, .cons x xs, ys => .cons x (_ : Vect α (n.plusL k))

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusL n k)

appendL を再帰的に呼び出すことで、目的の長さの Vect を構築することができます：

def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
  | 0, k, .nil, ys => ys
  | n + 1, k, .cons x xs, ys => .cons x (appendL n k xs ys)

これでプログラムが完成したので、n と k への明示的なマッチを削除することで読みやすく、関数も呼び出しやすくなります：

def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
  | .nil, ys => ys
  | .cons x xs, ys => .cons x (appendL xs ys)

definitional equality を使った型の比較は関数定義の内部を含め、definitionally equal なものに関連するすべてのものが、依存型と添字付けられた型の族を使うプログラムの インタフェース の一部になるということを意味します。型の中に関数の内部を公開するということは、その公開されたプログラムをリファクタリングすることでそれを使用するプログラムが型チェックをしなくなってしまう可能性があるということです。特に、plusL が appendL の型に使われているということは、plusL の定義を plusR と同等な他の定義に置き換えることができないということを意味します。

足し算での行き詰まり

appendを plusR で代わりに定義するとどうなるでしょうか？同じように始めると、それぞれのケースで長さとプレースホルダのアンダースコアが明示され、次のような有益なエラーメッセージが表示されます：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
  | 0, k, .nil, ys => _
  | n + 1, k, .cons x xs, ys => _

don't know how to synthesize placeholder
context:
α : Type u_1
k : Nat
ys : Vect α k
⊢ Vect α (Nat.plusR 0 k)

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusR (n + 1) k)

しかし、最初のプレースホルダを囲んで Vect α k の型注釈を付けようとすると、型の不一致エラーとなります：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
  | 0, k, .nil, ys => (_ : Vect α k)
  | n + 1, k, .cons x xs, ys => _

type mismatch
  ?m.3036
has type
  Vect α k : Type ?u.2973
but is expected to have type
  Vect α (Nat.plusR 0 k) : Type ?u.2973

このエラーは plusR 0 k と k が definitionally equal ではない ことを指摘しています。

これは plusR が次のような定義を持っているためです：

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

このパターンマッチは第1引数ではなく 第2 引数に対して行われるため、その位置に変数 k が存在すると簡約をすることができません。Leanの標準ライブラリにある Nat.add は plusL ではなく plusR と等価であるため、この定義で Nat.add を使おうとすると全く同じ問題が起こります：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n + k)
  | 0, k, .nil, ys => (_ : Vect α k)
  | n + 1, k, .cons x xs, ys => _

type mismatch
  ?m.3068
has type
  Vect α k : Type ?u.2973
but is expected to have type
  Vect α (0 + k) : Type ?u.2973

足し算は変数に つまって しまいます。これを解消するには、propositional equality を使用します。

Propositional Equality

propositional equality は2つの式が等しいという数学的な文です。definitional equality はLeanが必要な時に自動的にチェックする一種の曖昧な事実ですが、propositional equality の記述には明示的な証明が必要です。一度 propositional equality が証明されると、プログラム内でそれを使って型を修正し、等式を片方の辺を他方のもので置き換えることができ、型チェッカの詰まりを解消できます。

definitional equality がこのように限定されている理由は、アルゴリズムによるチェックを可能にするためです。 propositional equality はより機能が豊かですが、証明と称されるものが実際に証明であることを検証できたとしても、コンピュータは一般的に2つの式が命題的に等しいかどうかをチェックすることができません。definitional equality と propositional equality の断絶は人間と機械の間の分業を表現しています：退屈極まりない等式は definitional equality の一部として自動的にチェックされ、人間の頭脳は propositional equality で利用される興味深い問題に向けることができます。同様に、definitional equality は型チェッカによって自動的に呼び出されますが、propositional equality は明確に呼びかけなければなりません。

「命題・証明・リストの添え字アクセス」 にて、いくつかの同値についての文が simp を使って証明されました。これらの等式はすべて、propositional equality がすでに definitional equality になっているものです。一般的に、propositional equality についての文を証明するには、まずそれらを definitional equality か既存の証明済みの等式に近い形にし、simp のようなツールを使って単純化されたケースを処理します。simp タクティクは非常に強力です：裏では、高速で自動化された多くのツールを使って証明を構築します。これよりはシンプルな rfl と呼ばれるタクティクは propositional equality を証明するために definitional equality を使用します。rfl という名前は 反射律 （reflexivity）の略であり、すべてのものはそれ自身に等しいという同値についての性質です。

appendR の詰まりを解消するには、k = Nat.plusR 0 k という証明が必要ですが、これは plusR が第2引数の変数に着目しているため definitional equality ではないのでした。これを計算させるためには k を具体的なコンストラクタにしなければなりません。これはパターンマッチの仕事です。

特に、k は 任意の Nat でありうるので、このタスクは 任意の k に対して k = Nat.plusR 0 k であるという根拠を返す関数を必要とします。これは (k : Nat) → k = Nat.plusR 0 k という型を持つ同値の証明を返す関数でなければなりません。一番初めのパターンとプレースホルダから始めると、次のようなメッセージが返ってきます：

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => _
  | k + 1 => _

don't know how to synthesize placeholder
context:
⊢ 0 = Nat.plusR 0 0

don't know how to synthesize placeholder
context:
k : Nat
⊢ k + 1 = Nat.plusR 0 (k + 1)

パターンマッチによって k を 0 に絞り込むと、最初のプレースホルダは definitionally に成立する文の根拠となります。rfl タクティクはこれを処理し、残るは2番目のプレースホルダのみとなります：

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 => _

2番目のプレースホルダは少し厄介です。式 Nat.plusR 0 k + 1 は Nat.plusR 0 (k + 1) と definitionally equal です。これは、ゴールが k + 1 = Nat.plusR 0 k + 1 とも書けることを意味します：

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 => (_ : k + 1 = Nat.plusR 0 k + 1)

don't know how to synthesize placeholder
context:
k : Nat
⊢ k + 1 = Nat.plusR 0 k + 1

文の等式の両側にある + 1 の下には関数自体が返す別のインスタンスがあります。言い換えれば、k に対する再帰呼び出しは k = Nat.plusR 0 k という根拠を返すことになります。等式は関数の引数に適用されなければ等式になりません。つまり x = y ならば f x = f y となります。標準ライブラリには関数 congrArg があり、関数と同値の証明を受け取り、等号の両辺に関数を適用した新しい証明を返します。今回の場合、関数は (· + 1) です：

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 =>
    congrArg (· + 1) (plusR_zero_left k)

propositional equality は右向きの三角形の演算子 ▸ を使ってプログラムに導入することができます。同値の証明を第1引数に、他の式を第2引数に与えることで、この演算子は第2引数の型において等式の左辺のインスタンスを右辺の等式に置き換えます。つまり、以下の定義には型エラーがありません：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
  | 0, k, .nil, ys => plusR_zero_left k ▸ (_ : Vect α k)
  | n + 1, k, .cons x xs, ys => _

最初のプレースホルダは以下の型が期待されています：

don't know how to synthesize placeholder
context:
α : Type u_1
k : Nat
ys : Vect α k
⊢ Vect α k

これは ys で埋めることができます：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
  | 0, k, .nil, ys => plusR_zero_left k ▸ ys
  | n + 1, k, .cons x xs, ys => _

残りのプレースホルダを埋めるには、別の加算についてのインスタンスでの詰まりを解消する必要があります：

don't know how to synthesize placeholder
context:
α : Type u_1
n k : Nat
x : α
xs : Vect α n
ys : Vect α k
⊢ Vect α (Nat.plusR (n + 1) k)

ここで、証明すべき文は Nat.plusR (n + 1) k = Nat.plusR n k + 1 です。これは ▸ を使うことで + 1 を先頭に抜き出し、これによって cons のインデックスと一致させることができます。

この証明は plusR への第2引数、つまり k へのパターンマッチを行う再帰関数です。これは plusR 自身が第2引数でパターンマッチを行うためであり、証明はパターンマッチによって plusR を「解消」し、計算の挙動を明らかにすることができます。この証明の骨格は plusR_zero_left のものと非常によく似ています：

def plusR_succ_left (n : Nat) : (k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
  | 0 => by rfl
  | k + 1 => _

残ったケースの型は Nat.plusR (n + 1) k + 1 = Nat.plusR n (k + 1) + 1 と definitionally equal であるため、plusR_zero_left と同様に congrArg で解くことができます：

don't know how to synthesize placeholder
context:
n k : Nat
⊢ Nat.plusR (n + 1) (k + 1) = Nat.plusR n (k + 1) + 1

これによって証明が完成します：

def plusR_succ_left (n : Nat) : (k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
  | 0 => by rfl
  | k + 1 => congrArg (· + 1) (plusR_succ_left n k)

完成した証明は appendR の2番目のケースの詰まりを解くことに使うことができます：

def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
  | 0, k, .nil, ys => plusR_zero_left k ▸ ys
  | n + 1, k, .cons x xs, ys => plusR_succ_left n k ▸ .cons x (appendR n k xs ys)

再び appendR の長さの引数を暗黙にすると、証明の中で要求されていた明示的な名前がなくなります。しかし、これらの型をマッチさせるための値はほかにありえないため、Leanの型チェッカは裏で自動的にそれらを埋めるための情報を十分に持っています：

def appendR : Vect α n → Vect α k → Vect α (n.plusR k)
  | .nil, ys => plusR_zero_left _ ▸ ys
  | .cons x xs, ys => plusR_succ_left _ _ ▸ .cons x (appendR xs ys)

長所と短所

添字付けられた型の族には重要な特性があります：これらへのパターンマッチは definitional equality に影響を与えます。例えば、Vect に対する Match 式で nil のケースにおいて、長さは単純に 0 に なります 。definitional equality はとても便利です。というのもこれはいつでも有効であり、明示的に呼び出す必要がないからです。

しかし、依存型とパターンマッチによる definitional equality の使用にはソフトウェア工学的に重大な欠点があります。まず第一に、関数は型の中で使用する用として特別に書かなければならず、型の中で便利に使用される関数では最も効率的なアルゴリズムを使用していない可能性があります。一度型の中で関数が使用されて公開されると、その実装はインタフェースの一部となり、将来のリファクタリングが困難になります。第二に、definitional equality は時間がかかることがあります。2つの式が definitionally equal であるかどうかをチェックするよう求められた時で問題の関数が複雑で抽象化のレイヤーが多い場合、Leanは大量のコードを実行する必要がある可能性が発生します。第三に、definitional equality が失敗した時に得られるエラーメッセージは関数の内部的な用語で表現されるため、いつでも理解しやすいとは限りません。エラーメッセージに含まれる式の出所を理解するのは必ずしも容易ではありません。最後に、添字付けられた型の族と依存型関数のあつまりに自明でない不変量をエンコードすることはしばしば脆弱になります。関数の簡約についての挙動の公開によって便利な definitional equality を提供しないことが判明した際に、システムの初期の定義を変更しなければならないことがよくあります。別の方法として、等式の証明の要求をプログラムにちりばめることもできますが、これは非常に扱いにくくなる可能性があります。

慣用的なLeanのコードでは、添字付けられた型の族はあまり使われません。その代わりに、部分型と明示的な命題を使用して重要な不変性を強制することが一般的です。このアプローチでは明示的な証明が多く、definitional equality に訴えることはほとんどありません。対話型の定理証明器にふさわしく、Leanは明示的な証明を便利にするように設計されています。一般的に、ほとんどの場合においてこのアプローチが望ましいです。

しかし、データ型の添字付けられた型の族を理解することは重要です。plusR_zero_left や plusR_succ_left などの再帰関数は、実は 数学的帰納法による証明 （proofs by mathematical induction）です。再帰の基本ケースは帰納法の基本ケースに対応し、再帰呼び出しは帰納法の仮定に訴えることを表しています。より一般的には、Leanにおける新しい命題はしばしば帰納的な根拠の型として定義され、これらの帰納型は通常は添字を持ちます。定理を証明するプロセスはこの節の証明と同じようなプロセスで、実際にはこれらの型を持つ式を裏で構築しています。また、添字を持つデータ型はまさにその仕事に適したツールであることもあります。添字付きのデータ型の使い方を熟知することは、どのような場合に添字付きのデータ型を使うべきか知るための重要な要素です。

演習問題

• plusR_succ_left のスタイルの再帰関数を使って、すべての n と k に対して n.plusR k = n + k であることを証明してください。
• Vect 上の関数で plusL よりも plusR の方が自然であるものを書いてください。つまり plusL ではその定義を用いた証明が必要となるようなものです。