多態編碼的遞歸代數數據類型的值是什麼？

Question

以下問題與Recursive algebraic data types via polymorphism in Haskell有關。

遞歸代數數據類型可以通過使用通用參數多態性的系統F的功能以任何語言實現。例如，可以引入自然數的類型（在Haskell）作爲

newtype Nat = Nat { runNat :: forall t. (t -> (t -> t) -> t) } 

與「通常」的自然數n被實現爲

\ x0 f -> f(f(...(f x0)...)) 

與使用fn迭代。

同樣，布爾值的類型可以引入

newtype Bool = Bool { runBool :: forall t. t -> t -> t } 

與預期值「真」和「假」被實現爲

true = \ t f -> t 
false = \ t f -> f 

問：是否所有條款鍵入Bool或Nat或上述形式的任何其他可能的遞歸代數數據類型（以這種方式編碼），直到操作語義的一些減少規則？

實施例1（自然數）：是類型在某種意義上forall t. t -> (t -> t) -> t「等效」到窗體\ x0 f -> f (f (... (f x0) ...))的術語的任何術語？

實施例2（布爾）：在某種意義上類型的任何術語forall t. t -> t -> t '等效' 要麼\ t f -> t或\ t f -> f？

附錄（內部版）：如果所考慮的語言，甚至能表達命題平等的，這個薈萃數學問題可以內化爲如下，我會很高興，如果有人想出爲它的解決方案：

對於任何算符m我們可以定義通用模塊並在其上一些解碼 - 編碼的功能如下：

type ModStr m t = m t -> t 
UnivMod m = UnivMod { univProp :: forall t. (ModStr m t) -> t } 

classifyingMap :: forall m. forall t. (ModStr m t) -> (UnivMod m -> t) 
classifyingMap f = \ x -> (univProp x) f 

univModStr :: (Functor m) => ModStr m (UnivMod m) 
univModStr = \ f -> UnivMod $ \ g -> g (fmap (classifyingMap g) f) 

dec_enc :: (Functor m) => UnivMod m -> UnivMod m 
dec_enc x = (univProp x) univModStr 

Q ：如果語言能夠表達這種情況：是否相等型dec_enc = id居住？

Answer 1

在系統F（AKAλ2）的∀α.α→α→α所有居民確實λ - 等於K或K*。

首先，如果M : ∀α.α→α→α那麼它具有正常的形式N（因爲系統F被歸一化），並通過減少受試者定理（見Barendregt: Lambda calculi with types）也N : ∀α.α→α→α。讓我們來看看這些正常形式的外觀如何。 （我們將使用新一代引理λ2，看到Barendregt的書正式的細節。）

如果N是一個正常的形式，即N（或其任何子表達式）必須是在頭部正常形態，這是一個表達式形式λx1 ... xn. y P1 ... Pk，其中n和/或k還可以是0。

對於N的情況下，必須有至少一個λ，因爲最初我們沒有在打字上下文將結合的任何變量代替y。所以N = λx.U和x:α |- U:α→α。

現在再次出現必須是U的情況下，至少一個λ，因爲如果U只是y P1 ... Pk然後y將有一個函數類型（甚至對於k = 0我們需要y:α→α），但我們剛剛x:α在上下文中。所以N = λxy.V和x:α, y:α |- V:α。

但是V不能是λ..，因爲那麼它會有功能類型τ→σ。所以V必須只是形式z P1 ... Pk，但由於我們在上下文中沒有任何函數類型的變量，因此k必須爲0，因此V可能只有x或y。

因此，只有∀α.α→α→α類型的正常形式中有兩個術語：λxy.x和λxy.y，並且此類型的所有其他術語都等於這些術語中的一個。

---

使用類似的推理，我們可以證明的∀α.α→(α→α)→α所有居民都是β-等於教會的數字。 （我認爲，對於∀α.(α→α)→α→α類型的情況略差;我們還需要η平等，爲λf.f和λfx.fx對應1，但不是β-平等，公正βη相等）

Answer 2

如果我們忽視底部和unsafe的東西，那麼你可以通過功能a -> a進行通用的唯一的事情就是組成它們。然而，這並不完全阻止我們在有限的表達式上：我們也有無限構圖infty x f = f $ infty x f。

同樣，唯一的非遞歸布爾值確實\t _ -> t和\_ f -> f，但你也可以在這裏結繩，像

blarg t f = blarg (blarg t f) (blarg f t)