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.)
nie wiem zbyt wiele teorii, ale wnoszę, że dla bardziej dowcipnych języków, "Mu" jest najmniej ustalonym punktem, a "Nu" jest największym stałym punktem. W Haskell wszystkie te trzy mają być równoważne (jak sądzę).Zauważ, że bardzo łatwo zaimplementować 'cata' dla' Mu' i 'ana' dla' Nu'. – dfeuer
Spróbuj rozwiązać ten kata https://www.codewars.com/kata/folding-through-a-fixed-point/haskell – xgrommx