添字族

多相的な帰納型は型引数を取ります。例えば、List はリストの要素の型を、Except は例外や値の型をそれぞれ決定する引数を取ります。これらの型引数は対象のデータ型のすべてのコンストラクタで共有され、パラメータ と呼ばれます。

しかし、帰納型の引数はすべてのコンストラクタで同じである必要はありません。コンストラクタの選択によって型への引数が変化するような帰納型は 添字族 （indexed family）と呼ばれ、変化する引数は添字（index）と呼ばれます。添字族における「hello world」的教材は、要素の型に加えてリストの長さを含むリスト型であり、慣習的に「ベクトル」と呼ばれています：

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

関数宣言ではコロンの前にいくつかの引数を取り、定義全体で使用可能であることを示します。そしていくつかの引数はコロンの後ろに置き、この引数をパターンマッチの利用や関数ごとに定義できるようにしていることを示します。帰納的データ型でも同じ原理が働きます：引数 α がデータ型宣言の先頭かつコロンより前に来ている場合、これはパラメータで Vect 中のすべての定義の第一引数として提供されなければならないことを意味します。一方で、Nat 引数はコロンの後ろにあり、これは変化する可能性のあるインデックスであることを示します。実際、nil と cons コンストラクタの宣言の中で Vect が3回出現すると、それらすべてに一貫して α が第一引数として指定されますが、第二引数はそれぞれ異なります。

nil の宣言では、これが Vect α 0 型のコンストラクタであることが示されています。これは、ちょうど List String が期待されているコンテキストにおいて [1, 2, 3] がエラーになるように、Vect String 3 型が期待されているコンテキストで Vect.nil を使うと型エラーになるということです。

example : Vect String 3 := Vect.nil

type mismatch
  Vect.nil
has type
  Vect String 0 : Type
but is expected to have type
  Vect String 3 : Type

この例においての 0 と 3 の食い違いはこれら自体が型でないにもかかわらず、一般的な型のミスマッチとまったく同じ役割を果たします。

添字族は異なる添字の値によって使用できるコンストラクタを変えることができることから、型の族と呼ばれます。ある意味では、添字族は型ではありません；むしろ、関連した型のあつまりであり、添字の選択によってそのあつまりから型を選びます。 Vect において添字 5 を選ぶことによってコンストラクタは const のみ、また添字 0 を選ぶことによって nil のみがそれぞれ利用可能となります。

添字が不明である場合（例えば変数である等）、それが明らかになるまではどのコンストラクタも利用できません。長さとして n を用いると Vect.nil と Vect.cons のどちらも使用できません。というのも n が 0 と n + 1 のどちらにマッチする Nat を表すのかを知るすべがないからです：

example : Vect String n := Vect.nil

type mismatch
  Vect.nil
has type
  Vect String 0 : Type
but is expected to have type
  Vect String n : Type

example : Vect String n := Vect.cons "Hello" (Vect.cons "world" Vect.nil)

type mismatch
  Vect.cons "Hello" (Vect.cons "world" Vect.nil)
has type
  Vect String (0 + 1 + 1) : Type
but is expected to have type
  Vect String n : Type

型の一部でリストの長さを保持することはその型がより有益になることを意味します。例えば、Vect.replicate は与えられた値のコピー回数をもとに Vect を作る関数です。これを正確に表す型は以下のようになります：

def Vect.replicate (n : Nat) (x : α) : Vect α n := _

引数 n が結果の長さとして現れています。アンダースコアによるプレースホルダに紐づいたメッセージでは現在のタスクが説明されています：

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

添字族を扱う際に、コンストラクタはLeanがそのコンストラクタの添字が期待される型の添字と一致することを確認できた場合にのみ適用可能です。しかし、どちらのコンストラクタも n にマッチする添字を持っていません。nil は Nat.zero に、cons は Nat.succ にマッチします。型エラーの例のように、変数 n は関数に引数として渡される Nat によってこのどちらかを表す可能性があります。そこで解決策としてパターンマッチを使用してありうる両方のケースを考慮することができます：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => _
  | k + 1 => _

n は期待される型に含まれるため、n のパターンマッチによってマッチする2つのケースでの期待される型が 絞り込まれます 。1つ目のアンダースコアでは、期待される型は Vect α 0 になります：

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
⊢ Vect α 0

2つ目のアンダースコアでは Vect α (k + 1) になります：

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

パターンマッチが値の構造を解明することに加えてプログラムの型を絞り込む場合、これは 依存パターンマッチ （dependent pattern matching）と呼ばれます。

精練された型ではコンストラクタを適用することができます。1つ目のアンダースコアでは Vect.nil が、2つ目では Vect.cons がそれぞれマッチします：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons _ _

.cons の中にある1つ目のアンダースコアは α 型でなければなりません。ここで利用可能な α は存在しており、まさに x のことです：

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

2つ目のアンダースコアは Vect α k であるべきであり、これは replicate を再帰的に呼び出すことで生成できます：

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

以下が replicate の最終的な定義です：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons x (replicate k x)

関数を書く間の支援に加えて、Vect.replicate の情報に富んだ型によってクライアントコードはソースコードを読まなくても多くの予期しない関数である可能性を除外することができます。リスト用にした replicate では、間違った長さのリストを生成する可能性があります：

def List.replicate (n : Nat) (x : α) : List α :=
  match n with
  | 0 => []
  | k + 1 => x :: x :: replicate k x

しかし、このミスは Vect.replicate では型エラーになります：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons x (.cons x (replicate k x))

application type mismatch
  cons x (cons x (replicate k x))
argument
  cons x (replicate k x)
has type
  Vect α (k + 1) : Type ?u.1998
but is expected to have type
  Vect α k : Type ?u.1998

List.zip は2つのリストに対して、1つ目のリストの最初の要素と2つ目のリストの最初の要素をペアに、1つ目のリストの2番目の要素と2つ目のリストの2番目の要素をペアに、という具合に結合していく関数です。List.zip はオレゴン州の3つの最高峰とデンマークの3つの最高峰をペアにすることができます：

["Mount Hood",
 "Mount Jefferson",
 "South Sister"].zip ["Møllehøj", "Yding Skovhøj", "Ejer Bavnehøj"]

結果は3つのペアを含むリストです：

[("Mount Hood", "Møllehøj"),
 ("Mount Jefferson", "Yding Skovhøj"),
 ("South Sister", "Ejer Bavnehøj")]

リストの長さが異なる場合にどうすればいいかはやや不明確です。多くの言語のように、Leanは長い方のリストの余分な要素を無視する実装を選んでいます。例えば、オレゴン州の5つの最高峰の高度とデンマークの3つの最高峰の高度を組み合わせると3つのペアができます。具体的には：

[3428.8, 3201, 3158.5, 3075, 3064].zip [170.86, 170.77, 170.35]

は以下に評価されます。

[(3428.8, 170.86), (3201, 170.77), (3158.5, 170.35)]

このアプローチでは必ず答えが得られる点が便利である一方、意図せず長さの異なるリストを渡した際に情報が捨てられてしまう危険性があります。F#は別のアプローチをとっています：以下の fsi セッションで見られるように、F#での List.zip では長さが異なる場合は例外を投げます：

> List.zip [3428.8; 3201.0; 3158.5; 3075.0; 3064.0] [170.86; 170.77; 170.35];;

System.ArgumentException: The lists had different lengths.
list2 is 2 elements shorter than list1 (Parameter 'list2')
   at Microsoft.FSharp.Core.DetailedExceptions.invalidArgDifferentListLength[?](String arg1, String arg2, Int32 diff) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 24
   at Microsoft.FSharp.Primitives.Basics.List.zipToFreshConsTail[a,b](FSharpList`1 cons, FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 918
   at Microsoft.FSharp.Primitives.Basics.List.zip[T1,T2](FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 929
   at Microsoft.FSharp.Collections.ListModule.Zip[T1,T2](FSharpList`1 list1, FSharpList`1 list2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/list.fs:line 466
   at <StartupCode$FSI_0006>.$FSI_0006.main@()
Stopped due to error

これによって誤って情報が破棄される事態を避けられますが、その代わりにプログラムをクラッシュさせてしまうことにはそれなりの困難が伴います。Leanにおいて Option や Except モナドを使うような同じアプローチをすると安全性に見合わない負担が発生します。

しかし Vect を使えば、両方の引数が同じ長さであることを要求する型を持つバージョンの zip を書くことができます：

def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
  | .nil, .nil => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)

この定義は両方の引数が Vect.nil であるか、Vect.cons である場合のパターンを持っているだけであり、Leanは List に対する以下の同様の定義の結果のような missing cases エラーを出さずに定義を受け入れます：

def List.zip : List α → List β → List (α × β)
  | [], [] => []
  | x :: xs, y :: ys => (x, y) :: zip xs ys

missing cases:
(List.cons _ _), []
[], (List.cons _ _)

これは最初のパターンで使用されているコンストラクタ nil または cons が長さ n に関する型チェッカが持つ情報を洗練させるからです。最初のパターンが nil の場合、型チェッカは追加で長さが 0 であることを判断でき、その結果2つ目のパターンは nil 以外ありえなくなります。同様に、最初のパターンが cons の場合、型チェッカは Nat のある k に対して k + 1 の長さだったと判断することができ、2つ目のパターンは cons 以外ありえなくなります。実際、nil と cons を一緒に使うケースを追加すると、長さが一致しないために型エラーになります：

def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
  | .nil, .nil => .nil
  | .nil, .cons y ys => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)

type mismatch
  Vect.cons y ys
has type
  Vect β (?m.4718 + 1) : Type ?u.4530
but is expected to have type
  Vect β 0 : Type ?u.4530

n を明示的な引数にすることで、長さについての詳細化をより見やすくすることができます：

def Vect.zip : (n : Nat) → Vect α n → Vect β n → Vect (α × β) n
  | 0, .nil, .nil => .nil
  | k + 1, .cons x xs, .cons y ys => .cons (x, y) (zip k xs ys)

演習問題

依存型を使ったプログラミングの感覚をつかむには、この節の演習問題は非常に重要です。各演習問題において、コードを試しながら、型チェッカがどのミスを捉え、どのミスを捉えられないかを試行錯誤してみてください。これはエラーメッセージに対する感覚を養う良い方法でもあります。

オレゴン州の3つの最高峰とデンマークの3つの最高峰を組み合わせたときに Vect.zip が正しい答えを出すかダブルチェックしてください。Vect には List のような糖衣構文がないので、まず oregonianPeaks : Vect String 3 と danishPeaks : Vect String 3 を定義しておくと便利でしょう。

(α → β) → Vect α n → Vect β n 型を持つ Vect.map 関数を定義してください。

Vect の各要素を結合する際に関数を適用する関数 Vect.zipWith を定義してください。これは (α → β → γ) → Vect α n → Vect β n → Vect γ n 型になるべきです。

要素がペアである Vect を Vect のペアに分割する関数 Vect.unzip を定義してください。これは Vect (α × β) n → Vect α n × Vect β n 型になるべきです。

Vect の末尾に要素を追加する Vect.snoc を定義してください。これは Vect α n → α → Vect α (n + 1) 型になるべきで、#eval Vect.snoc (.cons "snowy" .nil) "peaks" は Vect.cons "snowy" (Vect.cons "peaks" (Vect.nil)) を返すべきです。snoc という名前は伝統的な関数型プログラミングのダジャレで、cons を逆さにしたものです。

Vect の順序を逆にする関数 Vect.reverse を書いてください。

次の型を持つ関数 Vect.drop を定義してください：(n : Nat) → Vect α (k + n) → Vect α k 。この関数が正しく動作することを検証するには #eval danishPeaks.drop 2 が Vect.cons "Ejer Bavnehøj" (Vect.nil) を返すことを確認することで行えます。

型 (n : Nat) → Vect α (k + n) → Vect α n で Vect の先頭から n 個の要素を返すの関数 Vect.take を定義してください。例をあげて動作することを確認もしてください。

Functional Programming in Lean 日本語訳

添字族

演習問題