Rekurencja polimorficzna - Polymorphic recursion
W informatyce , polimorficzne rekursji (określany również jako Milner - Mycroft typability lub rachunek Milner-Mycroft ) dotyczy rekursywnego parametrycznie polimorficzne funkcji , w którym zmienia się z każdym parametrem typu rekurencyjnego wywołania wykonany, zamiast pozostawania stałej. Wnioskowanie o typie dla rekurencji polimorficznej jest równoważne półunifikacji i dlatego jest nierozstrzygalne i wymaga użycia półalgorytmu lub adnotacji typu dostarczonych przez programistę .
Przykład
Zagnieżdżone typy danych
Rozważ następujący zagnieżdżony typ danych :
data Nested a = a :<: (Nested [a]) | Epsilon
infixr 5 :<:
nested = 1 :<: [2,3,4] :<: [[5,6],[7],[8,9]] :<: Epsilon
Funkcja długości zdefiniowana na tym typie danych będzie polimorficznie rekurencyjna, ponieważ typ argumentu zmieni się z Nested ana Nested [a]na w wywołaniu rekurencyjnym:
length :: Nested a -> Int
length Epsilon = 0
length (_ :<: xs) = 1 + length xs
Zauważ, że Haskell normalnie wywnioskuje sygnaturę typu dla funkcji tak prosto wyglądającej jak ta, ale tutaj nie można jej pominąć bez wywołania błędu typu.
Typy o wyższej randze
Aplikacje
Analiza programu
W analizie programowej opartej na typach rekurencja polimorficzna jest często niezbędna do uzyskania wysokiej precyzji analizy. Godne uwagi przykłady systemów wykorzystujących rekurencję polimorficzną obejmują analizę czasu wiązania Dussarta, Hengleina i Mossina oraz system zarządzania pamięcią oparty na regionie Tofte-Talpina . Ponieważ systemy te zakładają, że wyrażenia zostały już wpisane w bazowym systemie typów (niekoniecznie przy użyciu rekurencji polimorficznej), wnioskowanie może być ponownie rozstrzygane.
Struktury danych, wykrywanie błędów, rozwiązania grafowe
Struktury danych programowania funkcjonalnego często wykorzystują rekurencję polimorficzną, aby uprościć sprawdzanie błędów typów i rozwiązywać problemy za pomocą paskudnych „środkowych” rozwiązań tymczasowych, które pochłaniają pamięć w bardziej tradycyjnych strukturach danych, takich jak drzewa. W dwóch poniższych cytatach Okasaki (s. 144-146) podaje przykład CONS w Haskell, w którym system typów polimorficznych automatycznie oznacza błędy programisty. Aspektem rekurencyjnym jest to, że definicja typu zapewnia, że najbardziej zewnętrzny konstruktor ma jeden element, drugi parę, trzeci parę par itd. rekurencyjnie, ustawiając wzorzec automatycznego wyszukiwania błędów w typie danych. Roberts (s. 171) podaje pokrewny przykład w Javie , używający klasy do reprezentowania ramki stosu. Podany przykład jest rozwiązaniem problemu Wieży Hanoi, w którym stos symuluje rekurencję polimorficzną z początkową, tymczasową i końcową zagnieżdżoną strukturą zastępowania stosu.
Zobacz też
Uwagi
Dalsza lektura
- Meertens, Lambert (1983). „Przyrostowe sprawdzanie typu polimorficznego w B” (PDF) . Sympozjum ACM nt. Zasad Języków Programowania (POPL), Austin, Teksas .
- Mycroft, Alan (1984). Schematy typów polimorficznych i definicje rekurencyjne . Międzynarodowe Sympozjum Programowania, Tuluza, Francja . Notatki z wykładów z informatyki. 167 . s. 217-228. doi : 10.1007/3-540-12925-1_41 . Numer ISBN 978-3-540-12925-7.
- Henglein, Fritz (1993). „Wnioskowanie o typie z rekurencją polimorficzną”. Transakcje ACM dotyczące języków i systemów programowania . 15 (2): 253–289. CiteSeerX 10.1.1.42.3091 . doi : 10.1145/169701.169692 .
- Kfoury, AJ ; Tiuryn, J.; Urzyczyn P. (kwiecień 1993). „Rekonstrukcja typu w obecności rekurencji polimorficznej”. Transakcje ACM dotyczące języków i systemów programowania . 15 (2): 290–311. doi : 10.1145/169701.169687 . ISSN 0164-0925 .
- Michael I. Schwartzbach (czerwiec 1995). "Wnioskowanie o typie polimorficznym" . Raport techniczny BRICS-LS-95-3 .
- Emms, Marcin ; Leiß, Hans (1996). „Rozszerzenie funkcji sprawdzania typu dla SML o rekursję polimorficzną — dowód poprawności” . Raport techniczny 96-101 .
- Richard Bird i Lambert Meertens (1998). "Zagnieżdżone typy danych" .
- C. Vasconcellos, L. Figueiredo, C. Camarao (2003). „ Praktyczne wnioskowanie o typie dla rekurencji polimorficznej: implementacja w Haskell ”. Czasopismo Uniwersalnej Informatyki .
- L. Figueiredo, C. Camarao. „ Wnioskowanie o typie dla polimorficznych definicji rekurencyjnych: specyfikacja w Haskell ”.
- Hallett, J. J; Kfoury, AJ (lipiec 2005). „Przykłady programowania wymagające rekurencji polimorficznej” . Notatki elektroniczne w informatyce teoretycznej . 136 : 57–102. doi : 10.1016/j.entcs.2005.06.014 . ISSN 1571-0661 .
Linki zewnętrzne
 |
Ten komputer programowania artykuł związane z modelem jest en . Możesz pomóc Wikipedii, rozwijając ją . |