Algorytm W wykorzystujący schematy rekursji

Question

Chciałem móc sformułować algorytm wnioskowania typu tylnego milnera przy użyciu typów danych punktów stałych i schematów rekursji. Pomijając wszystkie szczegół oprócz rzeczywistych części rekursji:

w env term = case term of 
    Lam n e -> lam (w (modify1 env) e) 
    App a b -> app (w (modify2 env) a) (w (modify3 env) b) 
    ... 

Algorytm buduje strukturę danych środowisko env gdyż rekurencyjnie przemierza drzewa, aż osiągnie liście. Następnie używa tych informacji, ponieważ ponownie buduje wynik.

Bez części env można to łatwo zaimplementować za pomocą cata. Czy można to (z env) zrobić ogólnie za pomocą schematów rekursji?

Answer 1

Tak właśnie dokonać docelową cata funkcją Env -> a

- luqui

Tak, ale prawdopodobnie będziesz musiał użyć cata z wyższego rzędu typu nośnika, obliczanie działania, które może modyfikować środowisko i prawdopodobnie zawodzić.

- pigworker

Answer 2

bez części env, to może być łatwo realizowane z Cata. Czy to (z env) można zrobić ogólnie używając schematów rekursji?

To, czego szukasz, to chronomorphism. Pozwala to na rekursję przy użyciu zarówno wyników z przyszłości i przeszłości. Nie jest tak przyjazny dla użytkownika, jak się wydaje, ale jest to kanoniczny sposób robienia rzeczy przy użyciu schematów rekursji.