Polimorfizm parametryczny - Parametric polymorphism
Wielopostaciowość |
---|
Polimorfizm ad hoc |
Polimorfizm parametryczny |
Podpisywanie |
W języków programowania i teorii typów , polimorfizm parametryczny jest sposobem, aby język bardziej wyrazisty, jednocześnie zachowując pełną statycznych typu bezpieczeństwa . Korzystając z polimorfizmu parametrycznego , funkcja lub typ danych może być napisany ogólnie, aby mógł obsługiwać wartości identycznie, bez zależności od ich typu. Takie funkcje i typy danych nazywane są odpowiednio funkcjami ogólnymi i typami danych ogólnych i stanowią podstawę programowania generycznego .
Na przykład funkcja, append
która łączy dwie listy, może być skonstruowana tak, aby nie dbała o typ elementów: może dołączać listy liczb całkowitych , listy liczb rzeczywistych , listy łańcuchów i tak dalej. Niech zmienna type a oznacza typ elementów na listach. Następnie append
można wpisać
forall a. [a] × [a] -> [a]
gdzie [a]
oznacza typ list z elementami typu a . Mówimy, że typ append
jest parametryzowany przez a dla wszystkich wartości a . (Zauważ, że ponieważ istnieje tylko jeden typ zmiennej, funkcja nie może być zastosowana do dowolnej pary list: para, jak również lista wyników, muszą składać się z elementów tego samego typu) Dla każdego miejsca, w którym append
jest stosowana, wartość decyduje o .
Za Christopherem Stracheyem polimorfizm parametryczny można skontrastować z polimorfizmem ad hoc , w którym pojedyncza funkcja polimorficzna może mieć wiele odrębnych i potencjalnie niejednorodnych implementacji w zależności od typu argumentu (argumentów), do którego jest zastosowana. Zatem polimorfizm ad hoc może ogólnie obsługiwać tylko ograniczoną liczbę takich odrębnych typów, ponieważ dla każdego typu musi być zapewniona osobna implementacja.
Historia
Polimorfizm parametryczny został po raz pierwszy wprowadzony do języków programowania w ML w 1975 roku. Obecnie istnieje w Standard ML , OCaml , F# , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C++ i innych. Java , C# , Visual Basic .NET i Delphi wprowadziły "ogólne" dla polimorfizmu parametrycznego. Niektóre implementacje polimorfizmu typu są powierzchownie podobne do polimorfizmu parametrycznego, jednocześnie wprowadzając aspekty ad hoc. Jednym z przykładów jest specjalizacja szablonów C++ .
Najbardziej ogólną formą polimorfizmu jest „ impredykatywny polimorfizm wyższego rzędu ”. Dwa popularne ograniczenia tej formy to polimorfizm rang ograniczonych (na przykład polimorfizm rang-1 lub polimorfizm prenex ) i polimorfizm predykatowy. Łącznie te ograniczenia dają „predykatywny polimorfizm prenex”, który jest zasadniczo formą polimorfizmu występującego w ML i wczesnych wersjach Haskella.
Polimorfizm wyższego rzędu
Polimorfizm rangi-1 (prenex)
W systemie polimorficznym prenex zmienne typu nie mogą być tworzone z typami polimorficznymi. Jest to bardzo podobne do tego, co nazywa się „stylem ML” lub „polimorfizmem Let” (technicznie polimorfizm Let w ML ma kilka innych ograniczeń składniowych). To ograniczenie sprawia, że rozróżnienie między typami polimorficznymi i niepolimorficznymi jest bardzo ważne; zatem w systemach predykatywnych typy polimorficzne są czasami określane jako schematy typów, aby odróżnić je od zwykłych (monomorficznych), które są czasami nazywane monotypami . Konsekwencją jest to, że wszystkie typy można zapisać w formie, która umieszcza wszystkie kwantyfikatory na skrajnej pozycji (prenex). Rozważmy na przykład append
opisaną powyżej funkcję, która ma typ
forall a. [a] × [a] -> [a]
W celu zastosowania tej funkcji do pary list, typ musi zostać zastąpiony zmienną a w typie funkcji tak, aby typ argumentów odpowiadał wynikowemu typowi funkcji. W systemie imperatywnym podstawionym typem może być dowolny typ, w tym typ, który sam jest polimorficzny; w ten sposób append
można zastosować do par list z elementami dowolnego typu — nawet do list funkcji polimorficznych, takich jak ona append
sama. Polimorfizm w języku ML ma charakter predykatywny. Dzieje się tak, ponieważ predykatywność wraz z innymi ograniczeniami sprawia, że system typów jest na tyle prosty, że zawsze możliwe jest pełne wnioskowanie o typie .
Jako praktyczny przykład, OCaml (potomek lub dialekt ML ) wykonuje wnioskowanie o typie i obsługuje polimorfizm impredykatywny, ale w niektórych przypadkach, gdy używany jest polimorfizm impredykatywny, wnioskowanie o typie systemu jest niekompletne, chyba że programista dostarczył pewne jawne adnotacje typu.
Rank- k polimorfizm
Dla pewnej stałej wartości k polimorfizm rang- k jest systemem, w którym kwantyfikator może nie pojawiać się na lewo od k lub więcej strzałek (gdy typ jest narysowany jako drzewo).
Wnioskowanie o typie dla polimorfizmu rangi 2 jest rozstrzygalne, ale rekonstrukcja dla rangi 3 i wyższych już nie.
Polimorfizm rangi- n („wyższej rangi”)
Polimorfizm rang- n to polimorfizm, w którym kwantyfikatory mogą pojawiać się na lewo od dowolnej liczby strzałek.
Predykatywność i niepredykatywność
Polimorfizm predykatywny
W predykatywnym parametrycznym systemie polimorficznym typ zawierający zmienną typu nie może być używany w taki sposób, że jest instancją typu polimorficznego. Teorie typów predykatowych obejmują teorię typów Martina- Löfa i NuPRL .
Polimorfizm imperatywny
Polimorfizm impredykatywny (zwany także polimorfizmem pierwszej klasy ) jest najpotężniejszą formą polimorfizmu parametrycznego. Mówi się, że definicja jest nieprecyzyjna, jeśli jest autoreferencyjna ; w teorii typów pozwala to na utworzenie instancji zmiennej w typie dowolnym typem, w tym typami polimorficznymi, takimi jak on sam. Przykładem tego jest System F ze zmienną typu X w typie , gdzie X może nawet odnosić się do samego T.
W teorii typów najczęściej badane impredykatywne typowane rachunki λ są oparte na sześcianie lambda , zwłaszcza Systemu F .
Ograniczony polimorfizm parametryczny
W 1985 roku Luca Cardelli i Peter Wegner dostrzegli zalety zezwalania na ograniczenia parametrów typu. Wiele operacji wymaga pewnej znajomości typów danych, ale poza tym może działać parametrycznie. Na przykład, aby sprawdzić, czy element znajduje się na liście, musimy porównać elementy pod kątem równości. W Standard ML parametry typu postaci ''a są ograniczone tak, że operacja równości jest dostępna, stąd funkcja miałaby typ ''a × ''a lista → bool i ''a może być tylko typem ze zdefiniowaną równość. W Haskell ograniczenie jest osiągane przez wymaganie, aby typy należały do klasy typów ; zatem ta sama funkcja ma typ w Haskell. W większości języków programowania obiektowego, które obsługują polimorfizm parametryczny, parametry mogą być ograniczone do podtypów danego typu (zobacz Polimorfizm podtypów i artykuł Programowanie ogólne ).
Zobacz też
Uwagi
Bibliografia
-
Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (notatki do wykładu), Kopenhaga: Międzynarodowa Szkoła Letnia w Programowaniu Komputerowym. Opublikowane w: Strachey, Christopher (2000). Obliczenia wyższego rzędu i symboliczne . 13 : 11–49. doi : 10.1023/A: 1010000313106 . Brakujące lub puste
|title=
( pomoc ) - Hindley, J. Roger (1969), „Główny schemat typu obiektu w logice kombinatorycznej”, Transactions of the American Mathematical Society , 146 : 29-60, doi : 10.2307/1995158 , JSTOR 1995158 , MR 0253905.
- Girard, Jean-Yves (1971). „Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Elimination des Coupures dans l'Analyse et la Théorie des Types”. Materiały z II Sympozjum Logiki Skandynawskiej (w języku francuskim). Amsterdam. s. 63-92. doi : 10.1016/S0049-237X(08)70843-7 .
- Girard, Jean-Yves (1972), Interprétation fonctionnelle et elimination des coupures de l'arytmétique d'ordre supérieur (praca doktorska) (w języku francuskim), Université Paris 7.
- Reynolds, John C. (1974), "Ku teorii struktury typu", Colloque Sur la Programmation , Wykład Notatki z Informatyki , Paryż, 19 : 408-425, doi : 10.1007/3-540-06859-7_148 , ISBN 978-3-540-06859-4.
- Milner Robin (1978). „Teoria polimorfizmu typów w programowaniu” (PDF) . Journal of Computer and System Sciences . 17 (3): 348–375. doi : 10.1016/0022-0000(78)90014-4 .
- Cardelli, Luca ; Wegner, Peter (grudzień 1985). „O zrozumieniu typów, abstrakcji danych i polimorfizmu” (PDF) . Ankiety ACM Computing . 17 (4): 471–523. CiteSeerX 10.1.1.117.695 . doi : 10.1145/6041.6042 . ISSN 0360-0300 .
- Pierce, Benjamin C. (2002). Typy i języki programowania . MIT Naciśnij. Numer ISBN 978-0-262-16209-8.