Jaki jest cel Rank2Types?

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?

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.

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 = Λt.λx: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:

(Λt.λx: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.

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.

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.

Slajdy z kursu Bryana O'Sullivana z kursu Haskell na Uniwersytecie Stanforda pomogły mi zrozumieć Rank2Types.

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.