Polimorfizm parametryczny - Parametric polymorphism

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, appendktó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 appendmożna wpisać

forall a. [a] × [a] -> [a]

gdzie [a]oznacza typ list z elementami typu a . Mówimy, że typ appendjest 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 appendjest 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 appendopisaną 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 appendmożna zastosować do par list z elementami dowolnego typu — nawet do list funkcji polimorficznych, takich jak ona appendsama. 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