Jestem prawie pewien, że wszyscy znają ogólne metody formularza:
T DoSomething<T>(T item)
Ta funkcja jest również nazywana parametrycznie polimorficzną (PP), w szczególności PP rangi 1 .
Powiedzmy, że tę metodę można przedstawić za pomocą obiektu funkcji formularza:
<T> : T -> T
Oznacza to, <T>
że pobiera jeden parametr typu i T -> T
oznacza, że pobiera jeden parametr typu T
i zwraca wartość tego samego typu.
W takim przypadku następowałaby funkcja PP rangi 2:
(<T> : T -> T) -> int
Funkcja sama nie przyjmuje parametrów typu, ale przyjmuje funkcję, która przyjmuje parametr typu. Możesz kontynuować iteracyjnie, dzięki czemu zagnieżdżanie jest coraz głębsze, uzyskując PP coraz wyższej rangi.
Ta funkcja jest naprawdę rzadka wśród języków programowania. Nawet Haskell domyślnie na to nie pozwala.
To jest użyteczne? Czy potrafi opisać zachowania, które trudno opisać inaczej?
Co to znaczy, że coś może być impredycyjne ? (w tym kontekście)
let sdff = (g : (f : <T> (e : T) => void) => void) => {}
Odpowiedzi:
Ogólnie rzecz biorąc, używasz polimorfizmu wyższego rzędu, gdy chcesz, aby osoba odbierająca mogła wybrać wartość parametru typu zamiast wywołującego . Na przykład:
Każda funkcja
g
, którą do tego przekazuję,f
musi być w stanie podać miInt
wartość pewnego typu, przy czym jedyne, cog
wie o tym typie, to to, że ma instancjęShow
. Więc są koszerne:Ale to nie są:
Jedną ze szczególnie użytecznych aplikacji jest stosowanie zakresu typów do wymuszania zakresu wartości . Załóżmy, że mamy obiekt typu
Action<T>
reprezentujący akcję, którą możemy uruchomić, aby wygenerować wynik typuT
, taki jak przyszłość lub wywołanie zwrotne.Załóżmy teraz, że mamy również taki,
Action
który może przydzielaćResource<T>
obiekty:Chcemy wymusić, aby zasoby te były wykorzystywane tylko w miejscu, w
Action
którym zostały utworzone, a nie dzielone między różnymi akcjami lub różnymi przebiegami tej samej akcji, aby akcje były deterministyczne i powtarzalne.Aby to osiągnąć, możemy użyć typów wyższego rzędu, dodając parametr
S
do typówResource
iAction
, który jest całkowicie abstrakcyjny - reprezentuje „zakres”Action
. Teraz nasze podpisy to:Teraz, gdy dajemy , jesteśmy pewni, że ponieważ parametr „zakres” jest w pełni polimorficzny, że nie może uciec ciało -SO dowolną wartość typu, który używa takich jak również nie może uciec!
runAction
Action<S, T>
S
runAction
S
Resource<S, int>
(W Haskell nazywa się to
ST
monadą, gdzierunAction
się ją nazywarunST
,Resource
nazywa sięSTRef
inewResource
nazywa sięnewSTRef
).źródło
ST
Monada jest bardzo interesującym przykładem. Czy możesz podać więcej przykładów, kiedy przydatny byłby polimorfizm wyższej rangi?data Fetch d = forall a. Fetch (d a) (MVar a)
, które jest parą żądania do źródła danychd
i gniazda do przechowywania wyniku. Wynik i boks muszą mieć pasujące typy, ale ten typ jest ukryty, więc możesz mieć heterogeniczną listę żądań do tego samego źródła danych. Teraz można użyć polimorfizmu wyższej rangi napisać funkcję, która pobiera wszystkie wnioski, biorąc pod uwagę funkcję, która pobiera jeden:fetch :: (forall a. d a -> IO a) -> [Fetch d] -> IO ()
.Polimorfizm wyższej rangi jest niezwykle przydatny. W Systemie F (podstawowy język typowanych języków FP, który znasz), jest to niezbędne do akceptowania „typowanych kodowań kościelnych”, tak jak programuje system F. Bez nich system F jest całkowicie bezużyteczny.
W Systemie F definiujemy liczby jako
Dodawanie ma typ
który jest wyższym typem rangi (
forall c.
pojawia się w tych strzałkach).To pojawia się także w innych miejscach. Na przykład, jeśli chcesz wskazać, że obliczenia są poprawnym stylem przekazywania kontynuacji (google „codensity haskell”), powinieneś to zrobić jako
Nawet mówienie o niezamieszkanym typie w Systemie F wymaga polimorfizmu wyższej rangi
Krótko mówiąc, pisanie funkcji w systemie czystego typu (System F, CoC) wymaga polimorfizmu wyższego rzędu, jeśli chcemy poradzić sobie z interesującymi danymi.
W szczególności w systemie F kodowania te muszą być „impredykatywne”. Oznacza to, że
forall a.
kwantyfikuje absolutnie wszystkie typy . Krytycznie obejmuje to właśnie ten typ, który definiujemy. Wforall a. a
którea
może rzeczywiście stać naforall a. a
raz! W językach takich jak ML tak nie jest, mówi się, że są „predykatywne”, ponieważ zmienna typu kwantyfikuje tylko na podstawie zestawu typów bez kwantyfikatorów (zwanych monotypami). Nasza definicjaplus
wymaganego impredicativity a także dlatego, że instancjac
wl : Nat
sięNat
!Na koniec chciałbym wymienić ostatni powód, dla którego chcielibyście zarówno impredykatywności, jak i polimorfizmu wyższej rangi, nawet w języku z dowolnie rekurencyjnymi typami (w przeciwieństwie do systemu F). W Haskell istnieje monada efektów zwana „monadą wątku stanu”. Chodzi o to, że monada wątku stanu pozwala mutować rzeczy, ale wymaga ucieczki, aby wynik nie był zależny od niczego zmiennego. Oznacza to, że obliczenia ST są zauważalnie czyste. Aby egzekwować ten wymóg, stosujemy polimorfizm wyższego rzędu
Zapewniając, że
a
jest to poza zakresem, w którym wprowadzamys
, wiemy, żea
oznacza to dobrze sformułowany typ, na którym nie można polegaćs
. Używamys
do parameryzowania wszystkich zmiennych w tym konkretnym wątku stanu, więc wiemy, żea
jest on niezależny od zmiennych, a zatem nic nie wymyka się z zakresu tegoST
obliczenia! Wspaniały przykład użycia typów w celu wykluczenia źle sformułowanych programów.Nawiasem mówiąc, jeśli chcesz poznać teorię typów, sugeruję zainwestowanie w dobrą książkę lub dwie. Trudno jest nauczyć się tych rzeczy w kawałkach. Sugerowałbym jedną z książek Pierce'a lub Harpera na temat teorii PL w ogóle (i niektórych elementów teorii typów). Książka „Zaawansowane tematy w typach i językach programowania” obejmuje również sporo teorii typów. Wreszcie „Programowanie w teorii typów Martina Lofa” to bardzo dobra ekspozycja na temat intensywnej teorii typów, którą nakreślił Martin Lof.
źródło