Jaki jest cel Rank2Types?


110

Nie jestem biegły w Haskellu, więc może to być bardzo łatwe pytanie.

Jakie ograniczenie językowe rozwiązuje Rank2Types ? Czy funkcje w Haskell nie obsługują już argumentów polimorficznych?


Jest to w zasadzie uaktualnienie z systemu typu HM do polimorficznego rachunku lambda aka. λ2 / System F. Należy pamiętać, że wnioskowanie o typie jest nierozstrzygalne w λ2.
Poscat

Odpowiedzi:


116

Czy funkcje w Haskell nie obsługują już argumentów polimorficznych?

Robią, ale tylko o randze 1. Oznacza to, że chociaż możesz napisać funkcję, która przyjmuje różne typy argumentów bez tego rozszerzenia, nie możesz napisać funkcji, która używa swojego argumentu jako różnych typów w tym samym wywołaniu.

Na przykład poniższej funkcji nie można wpisać bez tego rozszerzenia, ponieważ gjest używana z różnymi typami argumentów w definicji f:

f g = g 1 + g "lala"

Zauważ, że jest całkowicie możliwe przekazanie funkcji polimorficznej jako argumentu do innej funkcji. Więc coś takiego map id ["a","b","c"]jest całkowicie legalne. Ale funkcja może używać go tylko jako monomorficznego. W przykładzie mapużywa idtak, jakby miał typ String -> String. Oczywiście zamiast opcji można też przekazać prostą funkcję monomorficzną danego typu id. Bez parametru rank2types nie ma możliwości, aby funkcja wymagała, aby jej argument był funkcją polimorficzną, a zatem nie ma również możliwości użycia jej jako funkcji polimorficznej.


5
Aby dodać kilka słów łączących moją odpowiedź z tą: rozważmy funkcję Haskella f' g x y = g x + g y. Jego wywnioskowany typ rangi 1 to forall a r. Num r => (a -> r) -> a -> a -> r. Ponieważ forall aznajduje się poza strzałkami funkcji, wywołujący musi najpierw wybrać typ a; jeśli wybiorą Int, otrzymamy f' :: forall r. Num r => (Int -> r) -> Int -> Int -> r, a teraz ustaliliśmy gargument, aby mógł przyjąć, Intale nie String. Jeśli włączymy, RankNTypesmożemy dodać adnotację f'typu forall b c r. Num r => (forall a. a -> r) -> b -> c -> r. Nie można go jednak użyć - co by to gbyło?
Luis Casillas

166

Trudno jest zrozumieć polimorfizm wyższego rzędu, jeśli nie studiujesz bezpośrednio Systemu F , ponieważ Haskell został zaprojektowany tak, aby ukryć przed tobą szczegóły w interesie prostoty.

Ale ogólnie rzecz biorąc, ogólny pogląd jest taki, że typy polimorficzne nie mają tak naprawdę a -> bformy, jaką mają w Haskell; w rzeczywistości wyglądają tak, zawsze z wyraźnymi kwantyfikatorami:

id :: a.a  a
id = Λtx:t.x

Jeśli nie znasz symbolu „∀”, czyta się go jako „dla wszystkich”; ∀x.dog(x)oznacza „dla wszystkich x, x jest psem”. „Λ” to duża lambda, używana do abstrahowania od parametrów typu; druga linia mówi, że id jest funkcją, która przyjmuje typ t, a następnie zwraca funkcję sparametryzowaną przez ten typ.

Widzisz, w Systemie F nie możesz idod razu zastosować takiej funkcji do wartości; najpierw musisz zastosować funkcję Λ do typu, aby uzyskać funkcję λ, którą zastosujesz do wartości. Na przykład:

tx:t.x) Int 5 = x:Int.x) 5
                  = 5

Standardowy Haskell (tj. Haskell 98 i 2010) upraszcza to, ponieważ nie ma żadnego z tego typu kwantyfikatorów, wielkich lambd i aplikacji typu, ale za kulisami GHC umieszcza je za kulisami, gdy analizuje program pod kątem kompilacji. (Sądzę, że to wszystko jest czas kompilacji, bez narzutu czasu wykonania).

Ale automatyczna obsługa tego przez Haskella oznacza, że ​​zakłada ona, że ​​„∀” nigdy nie pojawia się w lewej gałęzi typu funkcji („→”). Rank2Typesi RankNTypeswyłącz te ograniczenia i pozwól ci zastąpić domyślne reguły Haskella dotyczące miejsca wstawiania forall.

Dlaczego chcesz to zrobić? Ponieważ pełny, nieograniczony System F jest niesamowicie potężny i może zrobić wiele fajnych rzeczy. Na przykład ukrywanie typów i modułowość można zaimplementować przy użyciu typów wyższego rzędu. Weźmy na przykład zwykłą starą funkcję następującego typu rzędu-1 (do ustawienia sceny):

f :: r.∀a.((a  r)  a  r)  r

Do użytku f, dzwoniący najpierw musi wybrać, jakie typy użyć do ri a, a następnie dostarczyć argumentu wynikowego typu. Możesz więc wybrać r = Inti a = String:

f Int String :: ((String  Int)  String  Int)  Int

Ale teraz porównaj to z następującym typem wyższego rzędu:

f' :: r.(∀a.(a  r)  a  r)  r

Jak działa tego typu funkcja? Cóż, aby go użyć, najpierw określ, jakiego typu chcesz użyć r. Powiedz, że wybieramy Int:

f' Int :: (∀a.(a  Int)  a  Int)  Int

Ale teraz ∀aznajduje się wewnątrz strzałki funkcji, więc nie możesz wybrać, jakiego typu chcesz użyć a; musisz zastosować f' Intfunkcję Λ odpowiedniego typu. Oznacza to, że implementacja f'wybierze typ do użycia a, a nie wywołującyf' . Wręcz przeciwnie, bez typów o wyższej randze dzwoniący zawsze wybiera typy.

Do czego to jest przydatne? Cóż, w rzeczywistości do wielu rzeczy, ale jeden pomysł jest taki, że można go użyć do modelowania rzeczy, takich jak programowanie obiektowe, w którym „obiekty” łączą pewne ukryte dane razem z pewnymi metodami, które działają na tych ukrytych. Na przykład obiekt z dwiema metodami - jedną zwracającą Inta drugą zwracającą a String, można zaimplementować z tym typem:

myObject :: r.(∀a.(a  Int, a -> String)  a  r)  r

Jak to działa? Obiekt jest zaimplementowany jako funkcja, która ma pewne wewnętrzne dane typu ukrytego a. Aby faktycznie użyć obiektu, jego klienci przekazują funkcję „wywołania zwrotnego”, którą obiekt wywoła za pomocą dwóch metod. Na przykład:

myObject String a. λ(length, name):(a  Int, a  String). λobjData:a. name objData)

Tutaj w zasadzie wywołujemy drugą metodę obiektu, taką, której typ jest a → Stringdla nieznanego a. Cóż, nieznane myObjectklientom; ale tych klientów wiem, z podpisem, że będą w stanie zastosować jedną z dwóch funkcji do niego i dostać OSOBĄ Intlub String.

Aby zobaczyć rzeczywisty przykład Haskella, poniżej znajduje się kod, który napisałem, kiedy się uczyłem RankNTypes. Implementuje typ o nazwie, ShowBoxktóry łączy razem wartość jakiegoś ukrytego typu wraz z jego Showwystąpieniem klasy. Zauważ, że w przykładzie na dole tworzę listę, ShowBoxktórej pierwszy element został utworzony z liczby, a drugi ze łańcucha. Ponieważ typy są ukrywane przy użyciu typów o wyższej randze, nie narusza to sprawdzania typów.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

PS: dla każdego, kto to czyta, kto zastanawiał się, jak to się ExistentialTypesdzieje w zastosowaniach GHC forall, uważam, że powodem jest to, że używa tego rodzaju techniki za kulisami.


2
Dzięki za bardzo rozbudowaną odpowiedź! (co, nawiasem mówiąc, również ostatecznie zmotywowało mnie do nauki prawidłowej teorii typów i Systemu F.)
Aleksandar Dimitrov

5
Jeśli masz existssłowo kluczowe, możesz zdefiniować typ egzystencjalny jako (na przykład) data Any = Any (exists a. a), gdzie Any :: (exists a. a) -> Any. Używając ∀xP (x) → Q ≡ (∃xP (x)) → Q, możemy wywnioskować, że Anymoże również mieć typ forall a. a -> Anyi forallstąd pochodzi słowo kluczowe. Uważam, że typy egzystencjalne zaimplementowane przez GHC są zwykłymi typami danych, które również zawierają wszystkie wymagane słowniki typeklas (nie mogłem znaleźć odniesienia, aby to potwierdzić, przepraszam).
Vitus

2
@Vitus: egzystencjalne elementy GHC nie są powiązane ze słownikami typeklas. Możesz mieć data ApplyBox r = forall a. ApplyBox (a -> r) a; kiedy dopasujesz wzorzec do ApplyBox f x, otrzymasz f :: h -> ri x :: hdla „ukrytego”, ograniczonego typu h. Jeśli dobrze rozumiem, przypadek słownika typeklas jest tłumaczony na coś takiego: data ShowBox = forall a. Show a => ShowBox ajest tłumaczony na coś takiego data ShowBox' = forall a. ShowBox' (ShowDict' a) a; instance Show ShowBox' where show (ShowBox' dict val) = show' dict val; show' :: ShowDict a -> a -> String.
Luis Casillas

To świetna odpowiedź, na którą będę musiał poświęcić trochę czasu. Myślę, że jestem zbyt przyzwyczajony do abstrakcji zapewnianych przez C # generics, więc brałem wiele z tego za pewnik, zamiast faktycznie rozumieć teorię.
Andrey Shchekin,

@sacundim: Cóż, „wszystkie wymagane słowniki typeklas” może również oznaczać brak słowników, jeśli ich nie potrzebujesz. :) Chodziło mi o to, że GHC najprawdopodobniej nie koduje typów egzystencjalnych poprzez typy o wyższym rankingu (tj. Transformacja, którą sugerujesz - ∃xP (x) ~ ∀r. (∀xP (x) → r) → r).
Vitus,

47

Odpowiedź Luisa Casillasa daje wiele świetnych informacji o tym, co oznaczają typy rangi 2, ale omówię tylko jeden punkt, którego nie omówił. Wymaganie, aby argument był polimorficzny, nie tylko pozwala na używanie go z wieloma typami; ogranicza również to, co ta funkcja może zrobić ze swoimi argumentami i jak może wygenerować swój wynik. Oznacza to, że daje dzwoniącemu mniej elastyczność. Dlaczego chcesz to zrobić? Zacznę od prostego przykładu:

Załóżmy, że mamy typ danych

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

i chcemy napisać funkcję

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

który przyjmuje funkcję, która ma na celu wybranie jednego z elementów podanej listy i zwrócenie IOakcji wystrzeliwania pocisków w ten cel. Moglibyśmy daćf prosty typ:

f :: ([Country] -> Country) -> IO ()

Problem w tym, że mogliśmy przypadkowo uciec

f (\_ -> BestAlly)

a wtedy mielibyśmy duże kłopoty! Dającyf typu polimorficznego rangi 1

f :: ([a] -> a) -> IO ()

w ogóle nie pomaga, ponieważ wybieramy typ, akiedy dzwonimy f, i po prostu specjalizujemy się w nim Countryi \_ -> BestAllyponownie używamy naszego złośliwego oprogramowania . Rozwiązaniem jest użycie typu rangi 2:

f :: (forall a . [a] -> a) -> IO ()

Teraz funkcja, którą przekazujemy, musi być polimorficzna, więc \_ -> BestAlly nie wpisujemy check! W rzeczywistości żadna funkcja zwracająca element nie znajdujący się na podanej liście nie będzie sprawdzać typu (chociaż niektóre funkcje, które wchodzą w nieskończone pętle lub generują błędy i dlatego nigdy nie zwracają).

Powyższe jest oczywiście wymyślone, ale odmiana tej techniki jest kluczem do zapewnienia STbezpieczeństwa monady.


18

Typy o wyższej randze nie są tak egzotyczne, jak wskazywały inne odpowiedzi. Wierz lub nie, ale wiele języków zorientowanych obiektowo (w tym Java i C #!) Je obsługuje. (Oczywiście nikt w tych społecznościach nie zna ich pod przerażająco brzmiącą nazwą „typy o wyższej randze”).

Przykład, który podam, to podręcznikowa implementacja wzorca Visitor, z którego korzystam cały czas w mojej codziennej pracy. Ta odpowiedź nie jest wprowadzeniem do schematu odwiedzin; wiedza ta jest łatwo dostępna gdzie indziej .

W tej głupiej wyimaginowanej aplikacji HR chcemy operować pracownikami, którzy mogą być pełnoetatowymi pracownikami stałymi lub tymczasowymi kontraktorami. Mój preferowany wariant wzorca Visitor (a właściwie ten, którego dotyczy RankNTypes) parametryzuje typ powrotu odwiedzającego.

interface IEmployeeVisitor<T>
{
    T Visit(PermanentEmployee e);
    T Visit(Contractor c);
}

class XmlVisitor : IEmployeeVisitor<string> { /* ... */ }
class PaymentCalculator : IEmployeeVisitor<int> { /* ... */ }

Chodzi o to, że wielu odwiedzających z różnymi typami zwrotów może operować na tych samych danych. Oznacza to, że nie IEmployeewolno wyrażać opinii na temat tego, co Tpowinno być.

interface IEmployee
{
    T Accept<T>(IEmployeeVisitor<T> v);
}
class PermanentEmployee : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
class Contractor : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}

Chciałbym zwrócić uwagę na typy. Zauważ, że IEmployeeVisitoruniwersalnie kwantyfikuje jego typ zwracany, podczas gdy IEmployeekwantyfikuje go wewnątrz swojej Acceptmetody - to znaczy na wyższym poziomie. Tłumaczenie niezgrabnie z C # na Haskell:

data IEmployeeVisitor r = IEmployeeVisitor {
    visitPermanent :: PermanentEmployee -> r,
    visitContractor :: Contractor -> r
}

newtype IEmployee = IEmployee {
    accept :: forall r. IEmployeeVisitor r -> r
}

Więc masz to. Typy o wyższej randze są wyświetlane w języku C # podczas pisania typów zawierających metody ogólne.


1
Chciałbym wiedzieć, czy ktoś inny napisał o obsłudze C # / Java / Blub dla typów o wyższej randze. Jeśli znasz, drogi czytelniku, takie zasoby, prześlij je mi!
Benjamin Hodgson


-2

Dla osób zaznajomionych z językami obiektowymi funkcja wyższego rzędu jest po prostu funkcją ogólną, która jako argument oczekuje innej funkcji ogólnej.

Np. W TypeScript możesz napisać:

type WithId<T> = T & { id: number }
type Identifier = <T>(obj: T) => WithId<T>
type Identify = <TObj>(obj: TObj, f: Identifier) => WithId<TObj>

Widzisz, jak ogólny typ funkcji Identifywymaga funkcji ogólnej tego typu Identifier? To sprawia, że Identifyfunkcja wyższego rzędu.


Co to dodaje do odpowiedzi Sepp2k?
dfeuer

Albo Benjamina Hodgsona, jeśli o to chodzi?
dfeuer

1
Myślę, że przegapiłeś punkt widzenia Hodgsona. Acceptma typ polimorficzny rzędu 1, ale jest to metoda IEmployee, która sama w sobie ma stopień 2. Jeśli ktoś mi da IEmployee, mogę go otworzyć i użyć jego Acceptmetody w dowolnym typie.
dfeuer

1
Twój przykład ma również rangę 2, jako Visiteeklasa, którą wprowadzasz. Funkcja f :: Visitee e => T ejest (po usunięciu cugru) zasadniczo f :: (forall r. e -> Visitor e r -> r) -> T e. Haskell 2010 pozwala uciec od ograniczonego polimorfizmu rangi 2, używając takich klas.
dfeuer

1
W forallmoim przykładzie nie możesz wypłynąć . Nie mam żadnego odniesienia, ale możesz znaleźć coś w "Scrap Your Type Classes" . Polimorfizm wyższego rzędu może rzeczywiście wprowadzić problemy ze sprawdzaniem typu, ale ograniczony sortowanie implicite w systemie klas jest w porządku.
dfeuer
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.