inductive data type

在 dependent type 語言裡面，data type 會變成 inductive data type，引入了更多的限制，而其中跟大小有關的限制就是這裡想要討論的。

Question. 在定義建構子時 `c : (T -> T) -> T` 有參數 $T^T$ ，試問 $T^T$ 有多大？

答案是不知道，因為我們根本還不知道 $T$ 到底是什麼。

當 $T$ 定義完畢之後，這個簽名用在函數上倒是沒有問題，因為其大小已經確定，不會遇到自我指涉引發的麻煩。

雖然可以用公理強迫 $T^T$ 有 size，但這樣做一來會破壞計算性；二來會顯著的複雜化 termination check。舉例來說，要是容許定義 c，就可以寫出

def foo (t : T) : T :=
  match t with
  | c f => f t

接著 foo (c foo) 就會陷入無限迴圈，為了要有強正規化，我們希望排除所有這類型的程式，比起一個一個去比對，直接禁止定義 c 這類的建構子可以更簡單的達成目的。Haskell/OCaml 的 data type 則不做此限制，因為它們不需要強正規化，這也是為什麼 dependent type 語言常説其 data type 是 inductive data type，並不輕易省略 inductive 這個詞，因為這樣定義的類型滿足 induction principle。

另外一提，Bauer 談到所有建構子都是為了符合 $c : \Pi_{x : B} (A \; x \to T) \to T$ 的形式，有興趣的讀者可以著手證明。此外 strictly positive 的遞迴定義可能更適合實現檢查機制。

Question. 在定義建構子時 c : (T -> T) -> T 有參數 TTT^TTT ，試問 TTT^TTT 有多大？

Question. 在定義建構子時 `c : (T -> T) -> T` 有參數 $T^T$ ，試問 $T^T$ 有多大？