爲什麼我們使用摺疊來編碼數據類型作爲函數？

Question

或者具體而言，爲什麼我們使用foldr來編碼列表和迭代來編碼數字？

對不起，我很想知道如何命名我想問的事情，所以我需要首先給出一些說明。這從this C.A.McCann post吸引很大，只是不完全滿足我的好奇心，我也會用rank-n類型和無限懶惰的東西handwaving問題。

---

一個編碼數據類型作爲功能的方法是創建接收用於每種情況下一個參數是「圖案匹配」功能，每個變元爲接收對應於該構造，並返回一個相同的值的所有參數的函數結果類型。

這一切工作達到預期的非遞歸類型

--encoding data Bool = true | False 
type Bool r = r -> r -> r 

true :: Bool r 
true = \ct cf -> ct 

false :: Bool r 
false = \ct cf -> cf 

--encoding data Either a b = Left a | Right b 
type Either a b r = (a -> r) -> (b -> r) -> r 

left :: a -> Either a b r 
left x = \cl cr -> cl x 

right :: b -> Either a b r 
right y = \cl cr -> cr y 

然而，漂亮的類比模式匹配擊穿遞歸類型。我們也許會做這樣的事情

--encoding data Nat = Z | S Nat 
type RecNat r = r -> (RecNat -> r) -> r 
zero = \cz cs -> cz 
succ n = \cz cs -> cs n 

-- encoding data List a = Nil | Cons a (List a) 
type RecListType a r = r -> (a -> RecListType -> r) -> r 
nil = \cnil ccons -> cnil 
cons x xs = \cnil ccons -> ccons x xs 

，但我們不能在Haskell寫那些遞歸類型的定義！通常的解決方案是強制cons/succ案例的回調應用於所有級別的遞歸，而不僅僅是第一個（即寫一個fold/iterator）。在這個版本中，我們使用的返回類型r在遞歸類型是：

--encoding data Nat = Z | S Nat 
type Nat r = r -> (r -> r) -> r 
zero = \cz cf -> cz 
succ n = \cz cf -> cf (n cz cf) 

-- encoding data List a = Nil | Cons a (List a) 
type recListType a r = r -> (a -> r -> r) -> r 
nil = \z f -> z 
cons x xs = \z f -> f x (xs z f) 

雖然這個版本的作品，它使得定義一些功能更難。例如，如果你可以使用模式匹配，編寫一個列表的「尾部」函數或數字的「前輩」函數是微不足道的，但如果你需要使用摺疊，則會變得棘手。

所以到我真正的問題：

1. 我們怎樣才能確保在使用褶皺編碼是爲假想「模式匹配編碼」一樣強大？有沒有辦法通過模式匹配採取任意函數定義，並將其機械轉換爲僅使用摺疊的模式？ （如果是的話，這也將有助於使棘手的定義，例如尾巴或與foldl在foldr相似的條款少神奇）

2. 爲什麼不Haskell的類型系統允許在「模式匹配」所需的遞歸類型編碼？。是否有隻允許通過data定義的數據類型的遞歸類型的原因？模式匹配是直接使用遞歸代數數據類型的唯一方法嗎？它是否與類型推理算法有關？

Answer 1

上Scott encoding的維基百科頁面有一些有益的啓示。短版本是，你指的是教會的編碼，你的「假設模式匹配編碼」是斯科特編碼，兩者都是明智的做事方式，但教會編碼需要使用更輕型的機器（特別是，它不需要遞歸類型）。

兩個是均衡的證明uivalent使用以下想法：

churchfold :: (a -> b -> b) -> b -> [a] -> b 
churchfold _ z [] = z 
churchfold f z (x:xs) = f x (churchfold f z xs) 

scottfold :: (a -> [a] -> b) -> b -> [a] -> b 
scottfold _ z [] = z 
scottfold f _ (x:xs) = f x xs 

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b 
scottFromChurch f z xs = fst (churchfold g (z, []) xs) 
where 
    g x ~(_, xs) = (f x xs, x : xs) 

的想法是，既然churchfold (:) []是列出了身份，我們可以使用一個教會倍，產生的list參數它被賦予，以及它應該產生的結果。然後在鏈x1 `f` (x2 `f` (... `f` xn) ...)最外層f接收一對(y, x2 : ... : xn : [])（對於某些y我們不關心），這樣的回報f x1 (x2 : ... : xn : [])。當然，它也必須返回x1 : ... : xn : []，以便f的更多應用程序也可以工作。 （這實際上與「弱」或通常歸納原理的數學原理strong (or complete) induction的證明有些類似）。

順便說一句，你Bool r類型是有點太大，真正的教會布爾 - 例如(+) :: Bool Integer，但(+)不是真的教堂布爾。如果啓用RankNTypes，則可以使用更精確的類型：type Bool = forall r. r -> r -> r。現在，它被強制多態的，所以真正只有兩個（忽略seq和底部）的居民 - \t _ -> t和\_ f -> f。類似的想法也適用於你的其他教會類型。

Answer 2

鑑於一些感性的數據類型

data Nat = Succ Nat | Zero 

我們可以考慮在這個數據如何，我們的模式匹配

case n of 
    Succ n' -> f n' 
    Zero -> g 

它應該是顯而易見的Nat -> a類型的每個功能可以定義爲給出一個合適的f和g，並且製作Nat（baring bottom）的唯一方法是使用兩個c中的一個onstructors。

---

編輯：想想f片刻。如果我們通過給出適當的f和g使得f遞歸調用foo來定義函數foo :: Nat -> a，那麼我們可以將f重新定義爲f' n' (foo n')，使得f'不是遞歸的。如果類型a = (a',Nat)比我們可以改爲寫f' (foo n)。因此，不失一般性

foo n = h $ case n 
       Succ n' -> f (foo n) 
       Zero -> g 

這是把我的崗位是有意義的，其餘的配方：

---

因此，我們可以這樣思考的case語句作爲應用「析構函數字典「

data NatDict a = NatDict { 
    onSucc :: a -> a, 
    onZero :: a 
} 

現在我們從之前case語句可以成爲

h $ case n of 
     Succ n' -> onSucc (NatDict f g) n' 
     Zero -> onZero (NatDict f g) 

給定這一點，我們可以推導出

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a} 

那麼我們可以定義兩個函數

fromBB :: NatBB -> Nat 
fromBB n = cataNat n (NatDict Succ Zero) 

和

toBB :: Nat -> NatBB 
toBB Zero = Nat $ \dict -> onZero dict 
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict) 

我們可以證明這兩個函數都是見證的同構（最多加快和失去推理），並因此表明

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a) 

（這只是一樣NatBB）同構於Nat

我們可以使用與其他類型相同的構造，並證明所得到的函數類型是我們想要的只是證明的基本類型與代數推理（和歸納）同構。

至於你的第二個問題，Haskell的類型系統是基於iso-recursive而非equi-recursive類型的。這可能是因爲理論和類型推斷更容易用iso-recursive類型來解決，並且他們擁有所有的力量，他們只是給程序員部分增加了一點工作量。我喜歡說你可以得到你的異遞歸類型沒有任何開銷

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r) 

但顯然GHCs優化這些扼流圈有時:(。