Ed Kmett en <code>recursion-scheme</code> pakette Ed Kmett en tekrarlama düzeni paketinde

Question

yılında Fix, Mu ve Nu arasındaki fark üç beyanlar Ne var olan nedir?

Answer 1

Mu, katlama olarak yinelemeli bir türü temsil eder ve Nu, açıldığını gösterir. Haskell'de, bunlar izomorftur ve aynı türü temsil etmenin farklı yollarıdır. Eğer Haskell'in keyfi bir özyinelemeye sahip olmadığını iddia ediyorsanız, bu türler arasındaki ayrım daha ilginç hale gelir: Mu f en az (başlangıç) f sabit noktasıdır ve Nu f en büyük (uçbirim) sabit noktasıdır.

f sabit bir nokta, yani ters fonksiyonlar in :: f T -> T, out :: T -> f T bir çift tip TT ve f T arasında bir izomorfizm vardır. Fix tipi sadece, doğrudan izomorfizmi ilan etmek için Haskell'in yerleşik tipi özyinesini kullanır. Ancak hem Mu hem de Nu için giriş/çıkış yapabilirsiniz.

Somut bir örnek için, bir an için yinelemeli değerler yazamayacağınızı varsayın. Mu Maybe, yani :: forall r. (Maybe r -> r) -> r değerlerine sahip olanlar, doğal olanlardır, {0, 1, 2, ...}; Nu Maybe'un sakinleri, yani :: exists x. (x, x -> Maybe x) değerleri, {0, 1, 2, ..., ∞} conaturallarıdır. Nu Maybe'un neden fazladan bir sakinin olduğunu görmek için bu türlerin olası değerlerini düşünün.

bu türleri için bazı sezgi almak istiyorsanız, bir eğlence egzersiz (kabaca zorluk artan sırada) özyineleme olmadan aşağıdakileri uygulamak olabilir:

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)

Ayrıca şu uygulamaya çalışıyorum, ama onlar Özyinelemeyi gerektirir:

• nuToFix :: Nu f -> Fix f, fixToMu :: Fix f -> Mu f

Mu f az sabit noktasıdır ve Nu f olduğunu En büyük, bu yüzden :: Mu f -> Nu f bir fonksiyon yazmak çok kolay, ama bir fonksiyon yazıyor :: Nu f -> Mu f serttir; Akıma karşı yüzmek gibi.

(az bir nokta ben bu tür daha ayrıntılı bir açıklama yazmak için anlamı, ama o bu biçim için biraz fazla uzun olabilir.)