Jaka jest różnica między Fix, Mu i Nu w Eda Kmett za rekurencji pakietu programu

Question

W recursion-scheme pakietu Eda Kmett, istnieją trzy deklaracje:

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 

Jaka jest różnica między tymi trzema typami danych?

Answer 1

reprezentuje typ rekursywny jako jego fałdę, a Nu reprezentuje go jako rozwinięcie. W Haskell są to izomorficzne i są różne sposoby reprezentowania tego samego typu. Jeśli udajesz, że Haskell nie ma arbitralnej rekurencji, różnica między tymi typami staje się bardziej interesująca: Mu f jest najmniejszym (początkowym) stałym punktem f, a Nu f jest jego największym (końcowym) punktem stałym.

stałą bazą f jest typu T izomorfizmem pomiędzy T i f T tj parą odwrotnych funkcji in :: f T -> T, out :: T -> f T. Typ Fix po prostu wykorzystuje wbudowaną rekursję typu Haskella do bezpośredniego deklarowania izomorfizmu. Ale możesz zaimplementować wejście/wyjście zarówno dla Mu i Nu.

Dla konkretnego przykładu udawaj chwilę, że nie możesz zapisać wartości rekursywnych. Mieszkańcy Mu Maybe, tj. Wartości :: forall r. (Maybe r -> r) -> r, są naturalnymi, {0, 1, 2, ...}; mieszkańcy Nu Maybe, tj. wartości :: exists x. (x, x -> Maybe x), są koninalami {0, 1, 2, ..., ∞}. Pomyśl o możliwych wartościach tych typów, aby dowiedzieć się, dlaczego Nu Maybe ma dodatkowego mieszkańca.

Jeśli chcesz trochę intuicji dla tych typów, może to być zabawa ćwiczenie do realizacji następuje bez rekursji (mniej więcej w kolejności rosnącej trudności):

• 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)

Można także spróbować wdrożyć te, ale wymagają one rekurencji:

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

Mu f jest najmniejszy punkt stały, a Nu f jest największy, więc pisanie funkcji :: Mu f -> Nu f jest bardzo łatwe, ale pisanie funkcji :: Nu f -> Mu f jest trudne; to jak pływanie pod prąd.

(w pewnym momencie miałem zamiar napisać bardziej szczegółowe wyjaśnienie tych typów, ale to może być trochę zbyt długo dla tego formatu.)