import FormalLab.TypeTheory.OperationalSemantics

/-!
# 第17章：System Fとインプレディカティブ多相

STLCの恒等項は、原子型、関数型、そのほかの各型について別々の型導出を持てました。しかし「全ての型
`X` について `X → X`」という一つの型を、STLCの内部で項へ与えることはできません。型を受け取る抽象と
型への適用を、項の抽象・適用とは別に加える必要があります。

System Fは型変数と全称型 `∀X. A` を持つ二階の型付きラムダ計算です。本章では型束縛にもde Bruijn添字を
用い、型の持ち上げと捕獲回避代入を定義します。多相恒等関数を一度構成し、原子型と関数型へ特殊化します。
最後にインプレディカティブな量化とLeanの宇宙多相を、量化対象と型検査上の階層から区別します。

## 型抽象と型適用を項構文へ加える

型と項を次の文法で生成します。`ΛX.t` は型抽象、`t[A]` は型適用です。小文字ラムダが項変数を束縛し、
大文字ラムダが型変数を束縛します。

$$
A,B ::= \iota\mid X\mid A\to B\mid\forall X.A,
$$

$$
t,u ::= x\mid\lambda x:A.t\mid t\,u\mid\Lambda X.t\mid t[A].
$$

型注釈を項へ含めるChurch流の構文を採用します。型抽象を一つ入ると、外側の型変数を指す添字は一つ
増えます。同時に、項変数の型注釈も新しい型束縛子の内側へ運ばなければなりません。
-/

namespace FormalLab.TypeTheory.SystemF

inductive Ty where
  | atom : Ty
  | var : Nat → Ty
  | arrow : Ty → Ty → Ty
  | all : Ty → Ty
  deriving DecidableEq, Repr

infixr:60 " ⟹ " => Ty.arrow

inductive Term where
  | var : Nat → Term
  | lam : Ty → Term → Term
  | app : Term → Term → Term
  | typeLam : Term → Term
  | typeApp : Term → Ty → Term
  deriving DecidableEq, Repr

/-!
## 型変数の捕獲を避ける

`shiftTyAbove amount cutoff A` は `cutoff` 以上の自由な型変数添字を持ち上げます。全称型の下では
新しい型変数が束縛されるのでcutoffも一つ増やします。型代入は対象より外側の添字を一つ下げ、
全称型の下へ置換型を運ぶときはその自由変数を持ち上げます。
-/

def shiftTyAbove (amount cutoff : Nat) : Ty → Ty
  | .atom => .atom
  | .var index => if cutoff ≤ index then .var (index + amount) else .var index
  | .arrow domain codomain =>
      .arrow (shiftTyAbove amount cutoff domain) (shiftTyAbove amount cutoff codomain)
  | .all body => .all (shiftTyAbove amount (cutoff + 1) body)

def shiftTy (type : Ty) : Ty :=
  shiftTyAbove 1 0 type

def substituteTy (index : Nat) (replacement : Ty) : Ty → Ty
  | .atom => .atom
  | .var found =>
      if found < index then .var found
      else if found = index then replacement
      else .var (found - 1)
  | .arrow domain codomain =>
      .arrow (substituteTy index replacement domain)
        (substituteTy index replacement codomain)
  | .all body => .all (substituteTy (index + 1) (shiftTy replacement) body)

def instantiate (body replacement : Ty) : Ty :=
  substituteTy 0 replacement body

example : instantiate (.var 0 ⟹ .var 0) .atom = (.atom ⟹ .atom) := rfl

example :
    instantiate (.all (.var 1 ⟹ .var 0)) (.var 0) =
      .all (.var 1 ⟹ .var 0) := rfl

/-!
二つ目の例では、置換型の自由な変数 `.var 0` が内側の `∀` に捕獲されません。全称型の下で
`shiftTy` されて `.var 1` となり、内側で束縛された `.var 0` と区別されます。型代入でも項代入と
同じ捕獲問題が生じ、束縛子の種類ごとに持ち上げを管理します。

## 型判断は二種類の文脈を持つ

型文脈の長さ `typeDepth` は利用できる型変数の数、`termTypes` は項変数へ割り当てた型の列です。
`WellFormed depth A` は、`A` の自由な型変数添字が `depth` 未満であることを確認します。
-/

structure Context where
  typeDepth : Nat
  termTypes : List Ty

inductive Lookup : List Ty → Nat → Ty → Prop where
  | zero : Lookup (A :: Γ) 0 A
  | succ : Lookup Γ index A → Lookup (B :: Γ) (index + 1) A

inductive WellFormed : Nat → Ty → Prop where
  | atom : WellFormed depth .atom
  | var : index < depth → WellFormed depth (.var index)
  | arrow : WellFormed depth A → WellFormed depth B → WellFormed depth (A ⟹ B)
  | all : WellFormed (depth + 1) body → WellFormed depth (.all body)

def liftTypeContext (Γ : Context) : Context :=
  { typeDepth := Γ.typeDepth + 1
    termTypes := Γ.termTypes.map shiftTy }

inductive HasType : Context → Term → Ty → Prop where
  | var : Lookup Γ.termTypes index A → HasType Γ (.var index) A
  | lam : WellFormed Γ.typeDepth A →
      HasType { Γ with termTypes := A :: Γ.termTypes } body B →
      HasType Γ (.lam A body) (A ⟹ B)
  | app : HasType Γ function (A ⟹ B) → HasType Γ argument A →
      HasType Γ (.app function argument) B
  | typeLam : HasType (liftTypeContext Γ) body A →
      HasType Γ (.typeLam body) (.all A)
  | typeApp : HasType Γ function (.all body) → WellFormed Γ.typeDepth argument →
      HasType Γ (.typeApp function argument) (instantiate body argument)

/-!
型抽象規則で項変数文脈にも `map shiftTy` が必要です。既存の項変数型に自由に現れる型変数を、新しい
型束縛子の外側を指すよう一段移すためです。項本体だけを型抽象の下へ移して文脈を据え置けば、同じ添字が
別の型変数を指してしまいます。

型抽象と型適用の規則は、項変数の抽象・適用とは別です。$Delta$ は型変数文脈、$Gamma$ は項変数文脈を表します。

$$
\frac{\Delta,X;\Gamma\vdash t:A}
     {\Delta;\Gamma\vdash\Lambda X.t:\forall X.A}
\qquad
\frac{\Delta;\Gamma\vdash t:\forall X.A\qquad\Delta\vdash B\;\mathsf{type}}
     {\Delta;\Gamma\vdash t[B]:A[B/X]}.
$$

## 多相恒等関数を一度だけ構成する

多相恒等関数は `ΛX. λx:X. x` です。その型は `∀X. X → X` であり、型適用によって一つの型を選びます。
-/

def emptyContext : Context :=
  { typeDepth := 0, termTypes := [] }

def polymorphicIdentity : Term :=
  .typeLam (.lam (.var 0) (.var 0))

theorem polymorphicIdentityHasType :
    HasType emptyContext polymorphicIdentity (.all (.var 0 ⟹ .var 0)) := by
  apply HasType.typeLam
  apply HasType.lam
  · exact .var (by decide)
  · exact .var .zero

theorem identityAtAtomHasType :
    HasType emptyContext (.typeApp polymorphicIdentity .atom) (.atom ⟹ .atom) := by
  exact .typeApp polymorphicIdentityHasType .atom

theorem identityAtArrowHasType :
    HasType emptyContext
      (.typeApp polymorphicIdentity (.atom ⟹ .atom))
      ((.atom ⟹ .atom) ⟹ (.atom ⟹ .atom)) := by
  exact .typeApp polymorphicIdentityHasType (.arrow .atom .atom)

/-- 全称型自身へも特殊化できることを、型導出として検査します。 -/
theorem identityAtUniversalHasType :
    HasType emptyContext
      (.typeApp polymorphicIdentity (.all (.var 0 ⟹ .var 0)))
      (.all (.var 0 ⟹ .var 0) ⟹ .all (.var 0 ⟹ .var 0)) := by
  exact .typeApp polymorphicIdentityHasType (.all (.arrow (.var (by decide)) (.var (by decide))))

/-!
STLCでは同じ生項へ二つの導出を別々に作りました。System Fでは型抽象を含む一つの項と一つの全称型を
先に構成し、型適用によって二つの特殊化を得ます。この違いは単なる記法短縮ではなく、型を入力とする
計算構造を対象言語へ加えた結果です。

## インプレディカティブ量化と宇宙多相を分ける

System Fの `∀X. A` では、量化した型変数 `X` を全称型自身を含むSystem Fの任意の型へ特殊化できます。
量化が属する集合と量化対象の範囲を同じ階層で許すこの性質を**インプレディカティブ**と呼びます。
一方、Leanの `universe u` は定義を複数の宇宙レベルで再利用する仕組みです。`Type u` を同じ
`Type u` の要素にするわけではなく、`Type u : Type (u+1)` という階層を保ちます。

`identityAtUniversalHasType` はこの自己適用可能な量化範囲を具体化します。ここで全称型を項として自分自身へ
適用しているのではなく、多相恒等項の型引数として全称型を選んでいます。インプレディカティブ性は無型の
自己適用や `Type : Type` を意味しません。

System Fの全称型、Leanの暗黙の宇宙引数、項レベルの依存関数型はどれも「一般性」に関わりますが、
量化している対象が異なります。型変数、宇宙レベル、項変数を一つの多相性としてまとめません。

## 要点

* System Fは項抽象・適用とは別に、型抽象・型適用と全称型を持つ。
* 型束縛の下では型変数と項変数文脈中の型を同時に持ち上げる。
* 多相恒等関数は一つの項 `ΛX. λx:X. x` と一つの型 `∀X. X → X` を持つ。
* インプレディカティブ量化は同じ型世界全体へ特殊化できるが、宇宙多相は階層を保存する。
* 多相型だけでは実装の一様性をまだ証明しておらず、論理関係とパラメトリシティが必要になる。

## 研究史と文献案内

二階の多相ラムダ計算はGirardの証明論的研究とReynoldsのプログラミング言語研究で独立に現れ、後に
System Fと呼ばれるようになりました。発見史を単一の起源へ還元しません。型付け、正規化、論理との対応を
証明論側から読むには [GLT89]、プログラミング言語の構文と操作的性質から読むには [TAPL02] を
参照してください。本章のde Bruijn実装は歴史的原体系の記法そのものではありません。

## 問題

### 型抽象の下で二つの添字を追う

型変数を一つ、項変数を二つ持つ文脈を作り、さらに `typeLam` の下へ移してください。型変数添字と
項変数添字を別々の列にし、`liftTypeContext` が項変数型へ施す `shiftTy` を一段ずつ計算します。
持ち上げを省いた誤った文脈で、どの `.var 0` の意味が変わるか示せば完了です。

### 多相関数を三つの型へ特殊化する

`polymorphicIdentity` を原子型、関数型、全称型自身へ型適用し、三つの `HasType` 導出を作ってください。
各場合に `instantiate` が計算する型を通常の記法へ戻します。三導出が一つの型抽象を共有する点と、
STLCで三つの型導出を別々に与える場合の差を説明してください。

### 一様性が型付けだけから読めるか検討する

閉じた項が `∀X. X → X` を持つとき、各型で異なる処理を選べる構文がSystem Fにあるかを規則から
調べてください。型検査時の型情報と実行時の項構文を区別し、恒等性を結論するために必要な関係解釈を
予想します。宇宙多相との比較表に量化対象、階層、実行時情報、許される特殊化を含めれば完了です。
-/

end FormalLab.TypeTheory.SystemF