Add Append/HAppend type class pages explaining why ++ is used instead of +

LeanByExample/SUMMARY.lean

@@ -131,6 +131,7 @@
 - [型クラス](./TypeClass/README.md)
   - [Add: 閉じた + 演算用の記法クラス](./TypeClass/Add.md)
   - [Alternative: 回復可能な失敗](./TypeClass/Alternative.md)
+  - [Append: 閉じた ++ 演算用の記法クラス](./TypeClass/Append.md)
   - [Applicative: アプリカティブ関手](./TypeClass/Applicative.md)
   - [BEq: Bool値の比較](./TypeClass/BEq.md)
   - [Coe: 型強制](./TypeClass/Coe.md)
@@ -141,6 +142,7 @@
   - [Functor: 関手](./TypeClass/Functor.md)
   - [GetElem: n番目の要素を取得](./TypeClass/GetElem.md)
   - [HAdd: 一般の + 演算用の記法クラス](./TypeClass/HAdd.md)
+  - [HAppend: 一般の ++ 演算用の記法クラス](./TypeClass/HAppend.md)
   - [HMul: 一般の * 演算用の記法クラス](./TypeClass/HMul.md)
   - [Inhabited: 有項にする](./TypeClass/Inhabited.md)
   - [LawfulApplicative: アプリカティブ則](./TypeClass/LawfulApplicative.md)

LeanByExample/Type/List.lean

@@ -46,7 +46,7 @@ example {α : Type} (x : α) (xs : List α) : List.cons x xs = x :: xs := by
 #guard "hello" :: ["world"] = ["hello", "world"]
 
 /- ## 連結
-リスト同士を順序を保ちながら連結するには、`List.append` 関数を使います。これは `Append` 型クラスのインスタンスになっているので、`++` という演算子で利用できます。
+リスト同士を順序を保ちながら連結するには、`List.append` 関数を使います。これは [`Append`](#{root}/TypeClass/Append.md) 型クラスのインスタンスになっているので、`++` という演算子で利用できます。
 -/
 -- `++` 演算子が利用できる
 example {α : Type} (xs ys : List α) : xs ++ ys = List.append xs ys := by

LeanByExample/Type/String.lean

@@ -10,7 +10,7 @@
 #guard "Hello".toList = ['H', 'e', 'l', 'l', 'o']
 
 /- ## 文字列結合
-`String.append` を使って文字列を結合することができます。この関数は `++` という記号が割り当てられています。
+`String.append` を使って文字列を結合することができます。この関数は [`Append`](#{root}/TypeClass/Append.md) 型クラスのインスタンスになっているので、`++` という記号で利用できます。
 -/
 
 #guard String.append "Hello, " "world!" = "Hello, world!"

LeanByExample/TypeClass/Append.lean

@@ -0,0 +1,51 @@
+/- # Append
+
+`Append` は `++` という二項演算子のための型クラスです。ここまで [`HAppend`](#{root}/TypeClass/HAppend.md) と同じですが、`HAppend` は異なるかもしれない型 `α, β, γ` に対して連結 `(· ++ ·) : α → β → γ` を定義することができる一方で、`Append` は同じ型 `α` に対して連結 `(· ++ ·) : α → α → α` を定義することしかできません。
+
+`+` で表される演算は可換であることが期待される（`a + b = b + a`）のに対し、`++` で表される演算は一般に可換ではありません。たとえば、文字列やリストの連結は順序に依存するため非可換です。このような非可換な連結に `+` を使うと混乱を招くため、Lean では `++` という別の記法を用意しています。
+-/
+
+-- 文字列の連結は非可換: 順序が違うと結果が異なる
+#guard ("Hello, " ++ "world!" ≠ "world!" ++ "Hello, ")
+
+-- リストの連結も非可換
+#guard ([1, 2] ++ [3, 4] ≠ [3, 4] ++ [1, 2])
+
+-- 一方、自然数の足し算は可換
+#guard 2 + 3 = 3 + 2
+
+/- ## `Append` インスタンスを実装する -/
+
+/-- 自前で定義したリスト -/
+inductive MyList where
+  | nil
+  | cons (head : Nat) (tail : MyList)
+
+namespace MyList
+
+  def append (xs ys : MyList) : MyList :=
+    match xs with
+    | nil => ys
+    | cons x xs => cons x (append xs ys)
+
+  -- 記法が定義されていないので使えない
+  #check_failure MyList.nil ++ MyList.nil
+
+  -- `append` 関数を `++` の実装とする
+  instance : Append MyList where
+    append := append
+
+  -- 連結記号が使えるようになった
+  #check MyList.nil ++ MyList.nil
+
+end MyList
+
+/- ## 舞台裏
+`Append` 型クラスは、内部的には [`HAppend`](#{root}/TypeClass/HAppend.md) に展開されています。 -/
+
+-- #check コマンドの出力で記法を使わないようにする
+set_option pp.notation false in
+
+/-- info: HAppend.hAppend MyList.nil MyList.nil : MyList -/
+#guard_msgs in --#
+#check MyList.nil ++ MyList.nil

LeanByExample/TypeClass/HAppend.lean

@@ -0,0 +1,24 @@
+/- # HAppend
+
+`HAppend` (heterogeneous append) は、`++` という二項演算子のための型クラスです。
+`++` 記法が何を意味するかについての制約はありません。
+任意の型 `α, β, γ : Type` に対して連結 `(· ++ ·) : α → β → γ` を定義することができます。
+-/
+
+-- 最初は `++` 記号が定義されていないのでエラーになる
+#check_failure ([1, 2] ++ (3 : Nat))
+
+/-- HAppend 型クラスのインスタンスを実装する -/
+instance : HAppend (List Nat) Nat (List Nat) where
+  hAppend xs n := xs.concat n
+
+-- 連結記号が使えるようになった
+#guard [1, 2] ++ (3 : Nat) = [1, 2, 3]
+
+/- 標準ライブラリには、`Array α` に `List α` を連結して `Array α` を得る
+`HAppend (Array α) (List α) (Array α)` インスタンスが定義されています。-/
+
+-- Array に List を連結して Array を得ることができる
+#guard #[1, 2] ++ [3, 4] = (#[1, 2, 3, 4] : Array Nat)
+
+/- 連結 `(· ++ ·) : α → β → γ` が一つの型の中で閉じているとき、つまり `α = β = γ` のときは [`Append`](#{root}/TypeClass/Append.md) が使用できます。 -/