是什麼埃德Kmett的遞歸方案包

在埃德Kmett的recursion-scheme包修復，木，怒江之間的差異，有三個聲明：是什麼埃德Kmett的遞歸方案包

newtype Fix f = Fix (f (Fix f)) 

newtype Mu f = Mu (forall a. (f a -> a) -> a) 

data Nu f where 
    Nu :: (a -> f a) -> a -> Nu f

是什麼這三種數據類型之間的區別？

來源

2017-08-09 hgiesel

我不知道太多的理論，但據我瞭解，對於更多的校對語言，「Mu」是最不動的一點，Nu是最大的固定點。在Haskell中，這三者都應該是等同的（我相信）。請注意，'Mu'和'ana'爲'Nu'實現'cata'非常容易。 – dfeuer

嘗試解決這個卡塔https://www.codewars.com/kata/folding-through-a-fixed-point/haskell – xgrommx

Mu表示作爲其摺疊的遞歸類型，並且Nu表示其展開。在Haskell中，這些是同構的，並且是表示相同類型的不同方式。如果你假裝Haskell沒有任意遞歸，這些類型之間的區別變得更加有趣：Mu f是最小（初始）固定點f，並且Nu f是其最大（終端）固定點。

的f的固定點是一種類型TT和f T之間的同構，即雙反函數in :: f T -> T，out :: T -> f T。類型Fix只是使用Haskell的內置類型遞歸來直接聲明同構。但是你可以實現輸入/輸出Mu和Nu。

對於一個具體的例子，暫時假裝你不能寫遞歸值。 Mu Maybe的居民，即值:: forall r. (Maybe r -> r) -> r，是自然界{0,1,2，...}; Nu Maybe的居民，即值:: exists x. (x, x -> Maybe x)，是自然{0,1,2，...，∞}。想想這些類型的可能值，看看爲什麼Nu Maybe有一個額外的居民。

如果你想獲得一些直覺爲這些類型的，它可以是一個有趣的練習來實現，而不遞歸以下（大致在難度不斷增加的順序排列）：

zeroMu :: Mu Maybe，succMu :: Mu Maybe -> Mu Maybe
zeroNu :: Nu Maybe， succNu :: Nu Maybe -> Nu Maybe，inftyNu :: Nu Maybe
muTofix :: Mu f -> Fix f，fixToNu :: Fix f -> Nu f
inMu :: f (Mu f) -> Mu f，outMu :: Mu f -> f (Mu f)
inNu :: f (Nu f) -> Nu f，outNu :: Nu f -> f (Nu f)

您也可以嘗試來實現這些，但他們需要遞歸：

nuToFix :: Nu f -> Fix f，fixToMu :: Fix f -> Mu f

Mu f是最固定的點，Nu f是最大的，所以寫一個函數:: Mu f -> Nu f是很容易的，但是寫一個函數:: Nu f -> Mu f很難;這就像逆流而上。

（在一個點上，我的意思寫這些類型的更詳細的解釋，但它可能是這種格式有點太長了。）

來源

2017-08-09 04:08:07 shachaf

是什麼埃德Kmett的遞歸方案包

回答

相關問題