/-!
# 第40章：法則を持つ構造と型クラス探索

群や順序のような数学的構造は、台となる型だけでなく、演算と法則を一緒に持ちます。同じ定理を
多くの具体例へ適用するには、必要な構造を引数として受け取る必要があります。Leanの型クラスは
その構造値を探索して補いますが、探索機構そのものが数学的構造なのではありません。

本章ではまず演算と法則を通常の構造体へ束ね、次に `class`、`instance`、インスタンス引数を
導入します。明示的な引数と探索される引数を比較し、圏・関手・代数的構造をmathlibで扱う際に
「数学的仮定」と「elaboratorの選択」を分離して追えるようにします。

## 演算と法則を一つの構造に束ねる

数学的構造は、台となる対象、演算、指定された法則から成ります。たとえばinvolutionは
自己写像 `i : A → A` と法則 `∀x : A. i(i(x)) = x` の組です。この定義はLeanの
型クラス探索を前提としません。

依存対の記法を使えば、固定した型 $A$ 上のinvolution全体は

$$
\mathsf{Involution}(A)
\;=\;
\sum_{i:A\to A}\prod_{x:A} i(i(x))=x
$$

と表せます。第一成分の演算 $i$ によって、第二成分が証明すべき法則の命題が決まります。
構造体はこの依存する成分列へ名前付き射影を与える表現です。

## 構造値を型クラス探索で補う

Leanの構造体は複数の成分を一値に束ねます。`class` は構造体に探索対象という印を付け、
`[C α]` はelaboratorが探索して補うインスタンス引数です。

数学的定義は、どのデータと法則を一つの構造とするかを定めます。Leanのelaboratorは、
その構造を表す値を探索して引数へ渡します。構造体を`class`に変えても数学的法則は増えず、
既存の構造値を探索の候補にできるようになるだけです。

構造を調べるには、その値だけでなく構造を保存する写像も定めます。二つのinvolution
$(A,i)$、$(B,j)$ の間の準同型は、関数 $f:A\to B$ と可換条件

$$
f(i(x))=j(f(x))\qquad(x:A)
$$

から成ります。この条件は、台の関数が指定演算を忘れずに運ぶことを述べます。


-/

namespace FormalLab.TypeTheory.TypeClasses

universe u

/-! ## 演算と法則を一つの値に束ねる -/

/-- 二回適用すると元へ戻る自己関数を束ねた構造です。 -/
structure Involution (α : Type u) where
  act : α → α
  involutive : ∀ x, act (act x) = x

/-- 真偽反転は `Bool` 上のinvolutionです。 -/
def boolNotInvolution : Involution Bool where
  act := Bool.not
  involutive := by
    intro value
    cases value <;> rfl

/-- 二つのinvolutionの間で作用を保存する写像です。 -/
structure Involution.Hom {α : Type u} {β : Type u}
    (source : Involution α) (target : Involution β) where
  toFun : α → β
  map_act : ∀ x, toFun (source.act x) = target.act (toFun x)

/-- 恒等関数は任意のinvolutionの作用を保存します。 -/
def Involution.Hom.identity {α : Type u} (object : Involution α) :
    Involution.Hom object object where
  toFun := fun x => x
  map_act := fun _ => rfl

/-!
`boolNotInvolution.act` は計算に使うデータ成分、`involutive` は二回作用させると元へ戻る
という法則成分です。単に `Bool → Bool` を持つだけなら、定数関数も許されます。構造名に
ふさわしい法則をフィールドで要求することで、利用側は具体的な実装を知らずに法則を使えます。
-/

/-! ## 探索させる構造だけをclassにする -/

/-- 型 `α` に標準として選んだ一要素を持たせる、本章の最小例です。 -/
class ChosenElement (α : Type u) where
  chosen : α

instance : ChosenElement Nat where
  chosen := 0

instance : ChosenElement Bool where
  chosen := false

/-- 角括弧の引数は型 `α` から探索されます。 -/
def chosenElement (α : Type u) [ChosenElement α] : α :=
  ChosenElement.chosen

/-- 同じ構造値を通常の明示引数として受け取る版です。 -/
def chosenElementExplicit (α : Type u) (choice : ChosenElement α) : α :=
  choice.chosen

/-- 探索版は、見つかった構造値を明示版へ渡した項と同じです。 -/
theorem chosenElement_eq_explicit (α : Type u) [ChosenElement α] :
    chosenElement α = chosenElementExplicit α (inferInstance : ChosenElement α) :=
  rfl

#eval chosenElement Nat
#eval chosenElement Bool
#eval chosenElementExplicit Nat { chosen := 7 }

#synth ChosenElement Nat
#synth ChosenElement Bool

/-!
`chosenElement Nat` の表面構文には二つ目の引数がありませんが、elaboratorは型 `Nat` から
`ChosenElement Nat` のインスタンスを探索して挿入します。kernelが受け取る項では構造値が
実際の引数として存在します。型クラス探索はkernelの新しい推論規則ではなく、完全な項を
組み立てる前処理です。

`chosenElementExplicit Nat { chosen := 7 }` は、探索を使わず別の構造値を明示的に渡します。
この比較から、型クラスがグローバルな可変状態ではなく暗黙引数の合成機構だと分かります。

`chosenElement_eq_explicit` は辞書渡しを等式として露出させます。`inferInstance` はelaboratorに
構造値を合成させる要求であり、得られた値を `chosenElementExplicit` の通常引数へ渡します。
定理が `rfl` であることは、探索版の計算内容が特別なkernel規則ではなく同じ射影だと示します。
-/

/-!
## 数学的構造と探索機構

`ChosenElement` の要素を「単位元」とは呼びません。単位元であるには二項演算と左右単位律
が必要です。単に選ばれた値と、演算に対する数学的性質を名前で混同しないためです。

型クラスは数学的な集合のクラスでも、オブジェクト指向のサブタイプ関係でもありません。
構造値を合成し、暗黙に受け渡すelaboration上の仕組みです。インスタンスの選択は定理の
内容に影響するため、何を探索させるかはAPI設計の一部です。

一つの型に複数の自然な構造がある場合、どれを標準インスタンスにするかは慎重に決めます。
探索の失敗・循環・意図しないインスタンスは証明内容ではなくelaboration上の問題ですが、
本文の追跡可能性とAPIの可読性を大きく左右します。

## 要点

* 構造体はデータ・演算・法則を依存する名前付き成分として束ね、準同型は指定構造を保存する。
* `class` は構造体をインスタンス探索の対象にし、数学的意味を自動追加しない。
* `[C α]` は省略可能な実在の引数で、elaboratorが候補を探索して補う。
* 明示引数版と型クラス版は、構造値の渡し方が異なる。
* 探索させる標準構造の選択はAPI設計の一部である。

## 研究史と文献案内

Wadler–Blottの1989年論文 [WB89] は、型クラスをad-hoc polymorphismの機構として提示しました。
これはHindley–Milner多相性を拡張する提案です。Leanではこの系譜の探索機構を数学的構造の階層化にも用いますが、
Haskellの辞書変換と同じ言語・推論規則ではありません。数学的構造の定義と、構造値を自動で
補うelaborationを常に分離し、Leanの探索仕様は [LEAN-REF] で確認します。

## 問題

### 構造のデータと法則を読み分ける

`Involution` のフィールドをデータ成分と法則成分に分類し、各フィールドが後続の定理でどう使われるか
を追え。続いて二項演算、単位元、左右単位律をもつ構造を定義し、単に要素を一つ選ぶ
`ChosenElement` より何が強いかを説明する。

構造体が数学的構造を一つの型へ束ねることと、型クラス探索がその構造を暗黙に供給することは別の
機能である。この二点を、同じ構造を明示引数と型クラス引数の両方で受け取る関数により比較せよ。

### 省略された辞書を展開する

`chosenElement Nat` で省略された型クラス引数を完全な関数適用として書き、
`chosenElementExplicit` とkernelへ渡る項を比較せよ。`String` に空文字列を選ぶインスタンスも
定義し、探索に成功するまでの候補を確認する。

暗黙であることは存在しないことを意味しない。elaboratorが補った辞書が最終的な項のどこに現れ、
kernelが何を型検査するかを説明できれば完了である。

### インスタンス設計の曖昧さを診断する

同じ型に自然だと思える `ChosenElement` を二つ考え、どちらを大域的な標準インスタンスにするかで
プログラムの意味が変わる例を作れ。競合を局所インスタンスまたは明示引数で解消し、読者から選択が
見える設計と比較する。

型クラスは数学的に一意な構造を保証しない。探索の一意性、数学的対象の一意性、普遍性による同型を
区別し、後の圏論で構造保存写像を扱う準備として述べること。
-/

end FormalLab.TypeTheory.TypeClasses