List
List
は連結リストを表す型です。
Lean では次のように再帰的に定義されています。
/-- `α` 型の項を集めたリスト -/
inductive List.{u} (α : Type u) where
/-- 空リスト `[]` はリスト -/
| nil : List α
/-- `a : α` と `l : List α` があるとき、`a` を先頭に追加したリストが作れる -/
| cons (head : α) (tail : List α) : List α
List α
の項はカンマ区切りの値を []
で囲むことによって作ることができます。
#check ([1, 2, 3] : List Nat)
要素の追加
List α
の先頭に要素を追加した新しいリストを作るのは、::
という記法を使って行うことができます。
-- `::` で先頭に要素を追加する
#guard "hello" :: ["world"] = ["hello", "world"]
この操作は元のリストを変更しません。Lean は純粋関数型プログラミング言語であるため、一般にグローバル変数に対して破壊的な変更はできません。今後特に断らない限り、常に元のデータは変更されていないと思ってください。
#eval show IO Unit from
let xs := [1, 2, 3]
-- 先頭に 0 を追加
let _ys := 0 :: xs
-- xs は変更されていない
assert! xs = [1, 2, 3]
return ()
連結
リスト同士を順序を保ちながら連結するには、List.append
関数を使います。これには ++
という演算子が割り当てられています。
-- リストの連結
#guard [1.0, 2.0] ++ [3.0] == [1.0, 2.0, 3.0]
高階関数
「関数を引数に取る関数」や「関数を返す関数」のことを、高階関数と呼ぶことがあります。List
名前空間には様々な高階関数が定義されています。
map
List
は Functor
型クラスのインスタンスになっているため <$>
演算子が利用できます。
-- `<$>` 演算子が利用できる
#guard (fun x => x * 2) <$> [1, 2, 3] = [2, 4, 6]
f <$> xs
は List
においては List.map f xs
と解釈され、これは「リストの中身全部に関数を適用する」操作を表します。
variable {α β : Type}
/-- #### List.map の使用例
`xs.map f` は、関数 `f : α → β` をリスト `xs : List α` の各要素に適用して、
新しく `List β` の項を作る。
-/
example {a₁ a₂ a₃ : α} (f : α → β)
: [a₁, a₂, a₃].map f = [f a₁, f a₂, f a₃] := by
rfl
-- リストの各要素を 2 倍する
#guard List.map (fun x => x * 2) [1, 2, 3] = [2, 4, 6]
filter
List
の中の要素から、ある条件を満たすものだけを取り出すには List.filter
を使います。
-- `l` 以外の文字を残す
#guard ["h", "e", "l", "l", "o"].filter (· ≠ "l") = ["h", "e", "o"]
-- 偶数を残す
#guard [1, 2, 3, 4, 5].filter (· % 2 = 0) = [2, 4]
foldl と foldr
List.foldl
と List.foldr
は、リストの各要素を指定した二項演算で繋げます。
/-- `List.foldl` の例示のための型クラス -/
class Foldl (α β : Type) where
/-- 左結合的な二項演算 -/
op : α → β → α
-- 左結合的な演算子として `⊗` を定義する
@[inherit_doc] infixl:70 "⊗" => Foldl.op
/-- #### List.foldl の使用例
デフォルト値が `init : α` で、適用する二項演算が `⊗ : α → β → α` だとする。
また `⊗` は左結合的、つまり `a ⊗ b ⊗ c = (a ⊗ b) ⊗ c` であるとする。
このとき `[b₁, b₂, b₃] : List β` に対して、
`List.foldl` は左にデフォルト値を挿入して順に `⊗` を適用したものに等しい。
-/
example [Foldl α β] {b₁ b₂ b₃ : β} (init : α) :
[b₁, b₂, b₃].foldl (· ⊗ ·) init = init ⊗ b₁ ⊗ b₂ ⊗ b₃ := by
rfl
/-- `List.foldr` の例示のための型クラス -/
class Foldr (α β : Type) where
/-- 右結合的な二項演算 -/
op : α → β → β
-- 右結合的な演算子として `⋄` を定義する
@[inherit_doc] infixr:70 "⋄" => Foldr.op
/-- #### List.foldr の使用例
デフォルト値が `init : β` で、適用する二項演算が `⋄ : α → β → β` だとする。
また `⋄` は右結合的、つまり `a ⋄ b ⋄ c = a ⋄ (b ⋄ c)` であるとする。
このとき `[a₁, a₂, a₃] : List α` に対して、
`List.foldr` は右にデフォルト値を挿入して順に `⋄` を適用したものに等しい。
-/
example [Foldr α β] {a₁ a₂ a₃ : α} (init : β) :
[a₁, a₂, a₃].foldr (· ⋄ ·) init = a₁ ⋄ a₂ ⋄ a₃ ⋄ init := by
rfl
List.foldl
と List.foldr
の違いは、演算が左結合的と仮定するか右結合的と仮定するか以外にも、List.foldl
は末尾再帰(tail recursion)であるが List.foldr
はそうでないことが挙げられます。
/-- 自然数のリストの総和を計算する関数 -/
def List.sum' : List Nat → Nat
| [] => 0
| n :: ns => n + sum ns
/-- List.sum は List.foldr で表すことができる -/
example : List.foldr (· + ·) 0 = List.sum := by
-- 再帰的な定義を分解する
delta List.foldr List.sum
-- 両者は等しい
rfl
/-- 末尾再帰にした総和関数 -/
def List.sumTR (l : List Nat) : Nat :=
aux 0 l
where
-- ある初期値から始めてリストの各要素の総和を求めるヘルパ関数
aux : Nat → List Nat → Nat
| x, [] => x
| x, n :: ns => aux (x + n) ns
/-- List.sumTR は List.foldl で表すことができる -/
example : List.foldl (· + ·) 0 = List.sumTR := by
-- 再帰的な定義を分解する
delta List.foldl List.sumTR List.sumTR.aux
-- 両者は等しい
rfl