Czy przydatny jest polimorfizm parametryczny wyższego rzędu?

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 -> Toznacza, że ​​pobiera jeden parametr typu Ti 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)

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:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

Każda funkcja g, którą do tego przekazuję, fmusi być w stanie podać mi Intwartość pewnego typu, przy czym jedyne, co gwie o tym typie, to to, że ma instancję Show. Więc są koszerne:

f (length . show)
f (const 42)

Ale to nie są:

f length
f succ

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 typu T, taki jak przyszłość lub wywołanie zwrotne.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Załóżmy teraz, że mamy również taki, Actionktóry może przydzielać Resource<T>obiekty:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

Chcemy wymusić, aby zasoby te były wykorzystywane tylko w miejscu, w Actionktó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 Sdo typów Resourcei Action, który jest całkowicie abstrakcyjny - reprezentuje „zakres” Action. Teraz nasze podpisy to:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

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!runActionAction<S, T>SrunActionSResource<S, int>

(W Haskell nazywa się to STmonadą, gdzie runActionsię ją nazywa runST, Resourcenazywa się STRefi newResourcenazywa się newSTRef).

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

Nat = forall c. (c -> c) -> c -> c

Dodawanie ma typ

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

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

type CPSed A = forall c. (A -> c) -> c

Nawet mówienie o niezamieszkanym typie w Systemie F wymaga polimorfizmu wyższej rangi

type Void = forall a. a 

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. W forall a. aktóre amoże rzeczywiście stać na forall a. araz! 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 definicja pluswymaganego impredicativity a także dlatego, że instancja cw l : Natsię 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

runST :: forall a. (forall s. ST s a) -> a

Zapewniając, że ajest to poza zakresem, w którym wprowadzamy s, wiemy, że aoznacza to dobrze sformułowany typ, na którym nie można polegać s. Używamy sdo parameryzowania wszystkich zmiennych w tym konkretnym wątku stanu, więc wiemy, że ajest on niezależny od zmiennych, a zatem nic nie wymyka się z zakresu tego STobliczenia! 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.