Haskell 接受這兩種型別的定義
data PowerPower = PP ((PowerPower -> Bool) -> Bool)
data Power = P (Power -> Bool)
型別PowerPower在Reynolds 的論文中被廣泛使用，該論文駁斥了系統 F 的集合語意。它由這種型別的系統 F 表示
PowerPower = forall A, (((A -> Bool) -> Bool) -> A) -> A
PP = \ z A f -> f (\ u -> z (\ x -> u (x A f)))
雷諾茲的反駁以論證PowerPower與 的冪集的冪集同構而結束PowerPower，這與康托爾關于基數的定理相矛盾。兩個嵌套的冪集對應Bool于 的定義中的兩個箭頭PowerPower。
如果我們可以使用 typePower而不是PowerPower. 一個冪集足以應用康托定理。那么問題就變成了：我們可以Power在系統 F 中表示型別嗎？這可能很困難，因為Power的基礎型別函子\X -> (X -> Bool)是逆變的而不是協變的。由于 Haskell 接受 的定義Power，我們可以使用它在 Haskell 記憶體模型中的表示來派生 System F 中的型別。
uj5u.com熱心網友回復：
讓B任何型別（Bool，在你的情況下），并假設同構，其逆
iso :: P -> (P -> B)
osi :: (P -> B) -> P
現在，隨便拿f :: B->B。我們證明f有一個不動點。（這是 Lawvere 不動點定理的一個實體。）
定義
g :: P -> B
g p = f (iso p p)
然后我們有（我會讓你檢查以下內容是否正確）：
g (osi g) = f (iso (osi g) (osi g)) = f (g (osi g))
因此，g (osi g)是 的不動點f。
在 Haskell 中，這沒什么大不了的。畢竟，我們fix總是可以產生任何 end 的（最少）固定點f :: B->B。
然而，大多數型別的 lambda 演算，如簡單型別的 lambda 演算、系統 F、（歸納）構造的演算等，都在規范化。在那里，我們沒有任意遞回，并且每個（封閉）項的評估總是終止，減少到其具有規范形狀的正常形式。
如果我們取B = Bool, and f = not，我們有一個布林值b等于not b。這不會發生在這樣的演算中（Bool如果不存在則適當地擴展），因為b然后將歸一化為True或False，但兩者都不是固定點。
同樣，在 Haskell 中，我們可以采用非終止b = fix not，但在終止演算時我們沒有這樣的選擇。
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/316840.html
下一篇：更改控制器頁面的位置