import FormalLab.TypeTheory.LogicalRelations

/-!
# 第19章：パラメトリシティとfree theorem

型 `∀X. X → X` を持つ実装は、未知の型 `X` の値を調べる演算を受け取りません。直観的には入力を
そのまま返すしかありませんが、「他に書きようがない」という構文の眺めだけでは一般定理になりません。
型の全称量化を任意の関係の保存として解釈すると、この制約を方程式として取り出せます。

本章では全ての関係を保存する多相自己写像をLeanのメタレベルで定式化します。関数のグラフ関係から
自然性方程式を導き、さらに一点を指定する関係から任意の多相自己写像が恒等写像であることを証明します。
型だけから得られる定理の仮定と限界を明示し、型クラスによるad-hoc多相や型検査後の型情報観察と
混同しないようにします。

## 多相性を全ての関係の保存として仮定する

Leanの宇宙多相関数 `f : (α : Type u) → α → α` を考えます。型が似ているだけではSystem F項から
来たとは限らないため、任意の関係 `R` について `f R.Left` と `f R.Right` が `R` を保存するという
抽象化定理の結論を明示的な仮定にします。

$$
\mathsf{PreservesAllRelations}(f)
\;:\Longleftrightarrow\;
\forall A,B\;\forall R\subseteq A\times B\;\forall x,y,
\quad R(x,y)\Rightarrow R(f_A(x),f_B(y)).
$$
-/

namespace FormalLab.TypeTheory.Parametricity

open FormalLab.TypeTheory.LogicalRelations

universe u

def PreservesAllRelations (f : (α : Type u) → α → α) : Prop :=
  ∀ R : Relation, RelatedFunctions R R (f R.Left) (f R.Right)

/-!
`PreservesAllRelations f` はLeanの型だけからkernelが自動生成する性質ではありません。System Fの
抽象化定理を意味論的に移した仮定です。この境界を明示することで、Leanで定義できる全ての宇宙多相関数に
無条件でパラメトリシティを帰属させません。

## グラフ関係から自然性方程式を得る

任意の関数 `g : A → B` のグラフで `f A` と `f B` を関連づけます。入力 `x` と `g x` はグラフ関係に
あるため、出力も関連します。関係の定義を展開すると `g (f A x) = f B (g x)` が残ります。

$$
\operatorname{graph}(g)(x,g(x))
\Longrightarrow
\operatorname{graph}(g)(f_A(x),f_B(g(x)))
\Longrightarrow
g(f_A(x))=f_B(g(x)).
$$
-/

theorem commutesWithEveryFunction
    (f : (α : Type u) → α → α) (parametric : PreservesAllRelations f)
    {A B : Type u} (g : A → B) (x : A) :
    g (f A x) = f B (g x) := by
  have related := parametric (graphRelation g)
  exact related rfl

/-!
この式は `f` が全ての関数 `g` と可換することを述べます。圏論では恒等関手から自身への自然変換の
自然性に同じ形が現れますが、ここで使ったのは関係保存です。後の自然変換章で、対象・射・関手を備えた
圏論的定義と仮定の差を比較します。

## 一点を指定する関係から恒等性を導く

任意の型 `A` と要素 `x : A` を固定します。左を単位型、右を `A` とし、右要素が `x` であるときだけ
関連する関係を選びます。単位型側で `f` が何を返しても唯一の値です。関係保存により右側の `f A x` は
再び `x` と関連しなければならず、したがって `f A x = x` です。
-/

def pointRelation (A : Type u) (x : A) : Relation where
  Left := PUnit
  Right := A
  relates := fun _ y => y = x

theorem polymorphicEndomapIsIdentity
    (f : (α : Type u) → α → α) (parametric : PreservesAllRelations f)
    (A : Type u) (x : A) :
    f A x = x := by
  have related := parametric (pointRelation A x)
  have inputRelated : (pointRelation A x).relates PUnit.unit x := rfl
  exact related inputRelated

/-!
証明は関数の実装を場合分けしていません。任意関係を保存するという一様性から一点を固定する関係を選び、
その関係が出力にも保存されることだけを使います。これが型から導くfree theoremの最小例です。

$$
f:\forall X.\,X\to X
\quad\Longrightarrow\quad
\forall A\;\forall x:A,\ f_A(x)=x
$$

という結論は、ここでは任意関係を保存するという仮定の下で得られています。

`∀X. X → X` に発散や例外を加える言語では結論が変わり得ます。非停止計算を一つの結果とみなすなら、
恒等関数以外に常に発散する項が型を持てます。正格性、部分性、効果を関係解釈へ含めずに、純粋で
強正規化するSystem Fの結論を一般の言語へ移しません。

## 表現独立性はクライアントの観察を制限する

二つの実装型と、その間の表現関係を選びます。公開操作がその関係を保存し、クライアント項が抽象型に
対してパラメトリックなら、クライアントの結果も関係します。内部表現が自然数かリストかという差を、
公開インターフェースだけを使うクライアントは観察できません。

この論証では、操作ごとの関係保存がモジュール実装側の証明、基本補題がクライアント言語側の定理です。
「型が抽象だから安全」という標語だけでは、公開操作が表現関係を保存することも、観察の範囲も確定しません。

## ad-hoc多相との違い

型クラス制約を持つ関数は、型に応じた辞書を受け取って異なる処理を選べます。これは一つの実装を全ての
関係へ一様に適用するparametric polymorphismとは異なります。また実行時型表現、型キャスト、例外、
一般再帰を加えるとfree theoremの形を調整する必要があります。

## 要点

* パラメトリシティは多相項が任意の関係を保存するという抽象化定理で表される。
* 関数のグラフ関係を選ぶと、多相関数が任意の関数と可換する方程式を得る。
* 一点を指定する関係から `∀X. X → X` の実装が恒等的であることを導ける。
* free theoremは実装を見ずに型と関係解釈から得るが、純粋性・停止性・効果の仮定に依存する。
* 型クラスによるad-hoc多相は型依存の辞書を利用でき、parametric polymorphismとは異なる。

## 研究史と文献案内

Reynoldsの1983年論文 [REY83] は多相ラムダ計算の抽象化定理とparametric polymorphismを読む一次資料です。
Wadlerの1989年論文 [WAD89] は、型からプログラム方程式を導く方法を “theorems for free” として
広く展開しました。本章のLean定理は抽象化定理そのものの形式化ではなく、その関係保存結論から二つの
代表的帰結を導いたものです。System Fと論理関係の証明論的背景には [GLT89] を参照してください。

## 問題

### グラフ関係からfree theoremを導出する

`commutesWithEveryFunction` の証明を、関係の選択、入力の関連、出力の関連、方程式への展開という
四段階の数式へ戻してください。`g` を後者関数、リスト長、符号化関数へ変え、得られる等式を具体化します。
各具体化でグラフ関係の左右型を明記します。どの段階でも `f` の実装を使わず、型と関係保存だけを
使っていることを証明行ごとに確認すれば完了です。

### 一点関係の左右を変えて恒等性を再証明する

左を任意の型 `A`、右を単位型にした関係でも何が導けるか調べてください。次に本章の `pointRelation` を
真偽値で実装し、関係保存が `f A x = x` を強制する一段をLeanで再構成します。単位型の一意性を使う位置と、
右側の一点条件を使う位置を別々に示します。左右を交換した証明が同じ結論を与えるかを比較し、
与えない場合は量化のどの向きに情報が不足するか説明できれば完了です。

### 効果がfree theoremを変える反例を作る

発散、例外、実行時型検査のうち一つをSystem Fへ加えた仮想言語を選び、`∀X. X → X` の新しい閉項を
構成してください。本章のどの関係または基本補題がその項を排除できなくなるかを特定します。純粋な結論、
効果を含む修正版、必要な観察同値を比較し、仮定を省略しないfree theoremを書けば完了です。
-/

end FormalLab.TypeTheory.Parametricity