/-!
# 第31章：型族・依存関数型・依存対型

通常の関数型 `A → B` では、出力型 `B` は実際の入力を見ません。しかし長さ `n` の列を
受け取って同じ長さの列を返す関数や、命題 `P(x)` の証明を各 `x` について返す関数では、
結果の型が入力値を参照します。この依存を型式へ許すと、仕様の量化とデータの構造を同じ
言語で記述できます。

本章では型族を各点上のファイバーとして読み、依存関数型Πと依存対型Σを導入します。
定数族から通常の関数と直積を回収します。さらに全称・存在量化と形を比較し、保持する
計算情報の違いを明らかにします。これらがPTS、部分型、帰納族への共通基盤になります。

## 入力値が出力の型を決める

型族 `B : A → 𝒰` は、各 `a : A` に型 `B(a)` を割り当てます。`B(a)` を
`a` 上の**ファイバー**と呼びます。通常の関数が値から値へ進むのに対し、型族は値から
型へ進みます。依存型とは、型注釈を増やす技法ではなく、この値と型の依存辺を型式の中に
許す仕組みです。

* Π型 `Π(x : A). B(x)`：各 `x` に対し、そのファイバーの値を返す。
* Σ型 `Σ(x : A). B(x)`：あるタグ `x : A` と、そのファイバーの値 `B(x)` を一緒に持つ。

`β x` が `x` を使わない定数族なら、Π型は通常の関数型、Σ型は通常の直積型と同じ形に
戻ります。

$$
\prod_{x:A}B\;=\;A\to B,
\qquad
\sum_{x:A}B\;\simeq\;A\times B.
$$

Leanでは定数族のΠ型 `(x : A) → B` は、`x` が右辺に現れないため `A → B` の別表記です。
一方、`Sigma (fun _ : A => B)` と `A × B` は異なる帰納型なので定義的に同じではありませんが、
成分をそのまま移す標準的な同値を持ちます。

Π型とΣ型の形成・導入規則は、値の依存がどこに現れるかを示します。

$$
\frac{\Gamma\vdash A:\mathsf{Type}_u\qquad
      \Gamma,x:A\vdash B(x):\mathsf{Type}_v}
     {\Gamma\vdash \prod_{x:A}B(x):\mathsf{Type}_{\max(u,v)}}
$$

$$
\frac{\Gamma,x:A\vdash b(x):B(x)}
     {\Gamma\vdash \lambda x.b(x):\prod_{x:A}B(x)}
\qquad
\frac{\Gamma\vdash a:A\qquad\Gamma\vdash b:B(a)}
     {\Gamma\vdash \langle a,b\rangle:\sum_{x:A}B(x)}.
$$


-/

namespace FormalLab.TypeTheory.DependentTypes

universe u v

/-!
## 値によって結果が変わる型族を定義する

`Payload false` は計算すると `Nat`、`Payload true` は `Bool` になります。したがって
`defaultPayload false` と `defaultPayload true` は同じ関数の適用結果でも型が異なります。
これは実行時に型が曖昧になるという意味ではありません。引数を含む式を簡約することで、
kernelが各結果型を正確に計算できます。
-/

/-- タグが `false` なら `Nat`、`true` なら `Bool` を返す型族です。 -/
def Payload : Bool → Type
  | false => Nat
  | true => Bool

/-- 各タグに対し、対応するファイバーの値を返す依存関数です。 -/
def defaultPayload : (tag : Bool) → Payload tag
  | false => (0 : Nat)
  | true => false

#check defaultPayload false
#check defaultPayload true

/-!
## Π型：全ファイバーで一貫して働く

Π型にも通常の関数と同じ四つの見方があります。

* **形成**：`α : Type u` と `β : α → Type v` から `(x : α) → β x` を作る。
* **導入**：任意の `x` に対して `β x` の項を返すラムダ抽象を作る。
* **除去**：依存関数 `f` を `a : α` に適用し、`f a : β a` を得る。
* **計算**：`(fun x => body) a` は `body` の `x` を `a` で置換した式へ簡約する。

全称量化 `∀ x, p x` で学んだ証明の入出力は、終域が `Prop` であるΠ型そのものです。
-/

/-- 型族 `β` の各ファイバーで働く恒等関数です。 -/
def dependentIdentity {α : Type u} (β : α → Type v) :
    (x : α) → β x → β x :=
  fun _ value => value

/-- タグに応じて、対応する既定値を二つ並べた同じファイバーの積を返します。 -/
def duplicateDefault (tag : Bool) : Payload tag × Payload tag :=
  ⟨defaultPayload tag, defaultPayload tag⟩

/-!
## Σ型：タグと、そのタグで決まる値を隠さず保持する

通常の積 `α × β` では第二成分の型は第一成分と無関係です。Σ型では値 `⟨x, value⟩` の
第二成分が `β x` に属するため、第一成分が第二成分を型付けする情報を持ちます。タグだけを
取り出すのは簡単ですが、第二成分を固定型として返したければタグを調べて型族を簡約する
必要があります。
-/

/-- タグ `x` とファイバーの値をΣ型へ詰めます。 -/
def pack {α : Type u} {β : α → Type v} (x : α) (value : β x) : Sigma β :=
  ⟨x, value⟩

/-! ## 定数族では依存対と直積を相互に変換できる -/

/-- 定数族のΣ型を通常の直積へ送ります。 -/
def constantSigmaToProduct {α : Type u} {β : Type v} :
    (Sigma fun _ : α => β) → α × β :=
  fun value => ⟨value.1, value.2⟩

/-- 通常の直積を定数族のΣ型へ送ります。 -/
def productToConstantSigma {α : Type u} {β : Type v} :
    α × β → Sigma fun _ : α => β :=
  fun value => ⟨value.1, value.2⟩

/-- 往復しても依存対の値は変わりません。 -/
theorem productSigmaRoundTrip {α : Type u} {β : Type v}
    (value : Sigma fun _ : α => β) :
    productToConstantSigma (constantSigmaToProduct value) = value := by
  cases value
  rfl

/-- 逆向きの往復でも直積の値は変わりません。 -/
theorem sigmaProductRoundTrip {α : Type u} {β : Type v} (value : α × β) :
    constantSigmaToProduct (productToConstantSigma value) = value := by
  cases value
  rfl

/-- Σ型の値からタグを取り出します。 -/
def tag {α : Type u} {β : α → Type v} (value : Sigma β) : α :=
  value.1

def naturalPayload : Sigma Payload :=
  pack false (42 : Nat)

def booleanPayload : Sigma Payload :=
  pack true true

#check naturalPayload
#check booleanPayload
#check @dependentIdentity

/-!
Σ型の第二成分の型は第一成分に依存するため、タグを無視して常に同じ型として取り出す
ことはできません。タグを場合分けすれば、対応するファイバーが確定します。
-/

/-- タグを場合分けすることで、異なるファイバーの値を共通の文字列表現へ送ります。 -/
def showPayload : Sigma Payload → String
  | ⟨false, number⟩ => toString (show Nat from number)
  | ⟨true, boolean⟩ => toString (show Bool from boolean)

#eval showPayload naturalPayload
#eval showPayload booleanPayload

/-!
`showPayload` の各分岐では、第一成分のパターンによって第二成分の型も同時に精密化されます。
`false` 分岐の `number` は `Nat`、`true` 分岐の `boolean` は `Bool` です。依存対の除去は、
単に二成分を別々に取り出すより強く、両成分の依存関係を保存したまま場合分けします。

## 依存性が現れる場所

`∀ x, p x` は `p x : Prop` のΠ型です。一方 `∃ x, p x` は `Prop` に属し、証人を
計算データとして任意の `Type` へ取り出す用途には制限があります。`Sigma p` は
`p x : Type` のタグ付き計算データです。似た山括弧構文だけで同一視しません。

依存型は「型が実行時の任意の外部状態に依存する」という意味でもありません。型に現れる値は
Leanの項であり、型検査可能な依存として表現されます。どの計算を型検査中に許すかは理論と
kernelの設計に制約されます。

## 要点

* 型族は値ごとに型を割り当て、各結果型をファイバーと呼ぶ。
* Π型は各入力のファイバーから値を返し、Σ型はタグとそのファイバーの値を保持する。
* 定数族のΠ型は通常の関数型として書け、定数族のΣ型は通常の積型と標準的に同値である。
* 依存対を場合分けすると、タグの情報が第二成分の型を精密化する。
* `∀`・`∃` とΠ・Σは対応する形を持つが、`Prop` からの除去制限を無視して同一視しない。

## 研究史と文献案内

依存積・依存和は述語論理の量化とデータの型を同じ判断体系で扱います。Martin-Löf型理論
[ML84] は、その意味説明の基準文献です。ただし1972年版、1984年の講義録、1986年以後の
logical frameworkには差があります。Π・Σと構成的数学の関係は [ML84] が扱います。
プログラミング言語の依存的精密化は [PFPL16]、Leanの現行仕様は [LEAN-REF] を参照してください。

## 問題

### 定数族から通常の関数と対を復元する

型族 `B : A → Type` が定数関数 `fun _ => C` である場合、依存関数型と依存対型がそれぞれ
通常の `A → C` と `A × C` に対応することを、Π型・Σ型の数式とLeanの型の双方で示せ。
対応が定義的等しさなのか、同値による同一視なのかも確かめること。

`defaultPayload false` と `defaultPayload true` の型と値を計算し、同じ関数の結果型が入力値に
応じて変わることを確認せよ。通常の関数型だけではこの型をどう近似することになるかも述べる。

### 依存対を作り、添字に沿って除去する

`pack` の第二引数の型を明示し、第一引数を `false` と `true` に特殊化した型を別々に書け。
次に `Payload` の任意のファイバーの値を `Sigma Payload` に包む関数を定義し、その結果を
`showPayload` と同じ仕方で場合分けして利用せよ。

各分岐で第二成分の型がどのように精密化されるかを説明する。単にタグと値を格納するのではなく、
タグが値の型を決定し、除去時にもその関係が保存されることを示せれば完了である。

### 論理的存在と計算データを比較する

`∃ x, p x` と `Sigma fun x => p x` を、形成・導入・除去・宇宙の四点から比較せよ。証人を使って
新たなデータを計算する関数を一つ作り、命題の証明消去に課される制限と対照する。

両者をどちらも「証人と証拠の組」と説明できる一方、Leanで交換可能とは限らない。情報を消去して
よい命題と、実行時にも保持したいデータの違いを具体例に即して述べること。
-/

end FormalLab.TypeTheory.DependentTypes