Was ist der Zweck von Rank2Types?

Ich beherrsche Haskell nicht wirklich, daher könnte dies eine sehr einfache Frage sein.

Welche Sprachbeschränkung lösen Rank2Types ? Unterstützen Funktionen in Haskell nicht bereits polymorphe Argumente?

Unterstützen Funktionen in Haskell nicht bereits polymorphe Argumente?

Sie tun dies, aber nur von Rang 1. Dies bedeutet, dass Sie zwar eine Funktion schreiben können, die verschiedene Arten von Argumenten ohne diese Erweiterung akzeptiert, Sie jedoch keine Funktion schreiben können, die ihr Argument als verschiedene Typen in demselben Aufruf verwendet.

Beispielsweise kann die folgende Funktion ohne diese Erweiterung nicht eingegeben werden, da gsie bei der Definition von mit verschiedenen Argumenttypen verwendet wird f:

f g = g 1 + g "lala"

Beachten Sie, dass es durchaus möglich ist, eine polymorphe Funktion als Argument an eine andere Funktion zu übergeben. So etwas map id ["a","b","c"]ist also völlig legal. Die Funktion kann sie jedoch nur als monomorph verwenden. Im Beispiel wird mapverwendet, idals ob es Typ hätte String -> String. Und natürlich können Sie statt auch eine einfache monomorphe Funktion des angegebenen Typs übergeben id. Ohne rank2types gibt es keine Möglichkeit für eine Funktion, zu verlangen, dass ihr Argument eine polymorphe Funktion sein muss, und daher auch keine Möglichkeit, sie als polymorphe Funktion zu verwenden.

Es ist schwer, einen höherrangigen Polymorphismus zu verstehen, wenn Sie System F nicht direkt studieren , da Haskell die Details davon im Interesse der Einfachheit vor Ihnen verbergen soll.

Aber im Grunde ist die grobe Idee, dass polymorphe Typen nicht wirklich die a -> bForm haben, die sie in Haskell haben; In Wirklichkeit sehen sie so aus, immer mit expliziten Quantifizierern:

id :: ∀a.a → a
id = Λt.λx:t.x

Wenn Sie das Symbol "∀" nicht kennen, wird es als "für alle" gelesen. ∀x.dog(x)bedeutet "für alle x ist x ein Hund." "Λ" ist das Großbuchstaben Lambda, das zum Abstrahieren über Typparameter verwendet wird. In der zweiten Zeile heißt es, dass id eine Funktion ist, die einen Typ annimmt tund dann eine Funktion zurückgibt, die von diesem Typ parametrisiert wird.

Sie sehen, in System F können Sie eine solche Funktion nicht einfach idsofort auf einen Wert anwenden . Zuerst müssen Sie die Λ-Funktion auf einen Typ anwenden, um eine λ-Funktion zu erhalten, die Sie auf einen Wert anwenden. Also zum Beispiel:

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

Standard Haskell (dh Haskell 98 und 2010) vereinfacht dies für Sie, indem es keine dieser Typquantifizierer, Großbuchstaben und Typanwendungen hat, aber hinter den Kulissen setzt GHC sie ein, wenn es das Programm zur Kompilierung analysiert. (Ich glaube, das ist alles zur Kompilierungszeit, ohne Laufzeitaufwand.)

Haskells automatische Behandlung bedeutet jedoch, dass davon ausgegangen wird, dass "∀" niemals im linken Zweig eines Funktionstyps ("→") erscheint. Rank2Typesund RankNTypesschalten Sie diese Beschränkungen und ermöglichen es Ihnen Haskells Standardregeln für außer Kraft zu setzen , wo einfügen forall.

Warum willst du das tun? Weil das volle, uneingeschränkte System F hella mächtig ist und viele coole Sachen machen kann. Beispielsweise können das Ausblenden und die Modularität von Typen mithilfe von Typen mit höherem Rang implementiert werden. Nehmen Sie zum Beispiel eine einfache alte Funktion des folgenden Rang-1-Typs (um die Szene einzustellen):

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

Zur Verwendung fmuss der Aufrufer zuerst auswählen, für welche Typen er verwendet werden soll, rund adann ein Argument des resultierenden Typs angeben. So könnten Sie auswählen r = Intund a = String:

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

Aber vergleichen Sie das jetzt mit dem folgenden höherrangigen Typ:

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

Wie funktioniert eine solche Funktion? Um es zu verwenden, geben Sie zuerst an, für welchen Typ Sie es verwenden möchten r. Sagen wir, wir wählen Int:

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

Aber jetzt ∀abefindet sich der innerhalb des Funktionspfeils, sodass Sie nicht auswählen können, für welchen Typ Sie ihn verwenden möchten a. Sie müssen sich f' Intauf eine Λ-Funktion des entsprechenden Typs anwenden . Dies bedeutet, dass bei der Implementierung von ausgewählt f'wird, für welchen Typ verwendet werden soll a, nicht für den Aufrufer vonf' . Im Gegensatz dazu wählt der Anrufer ohne höherrangige Typen immer die Typen aus.

Wofür ist das nützlich? Nun, für viele Dinge tatsächlich, aber eine Idee ist, dass Sie dies verwenden können, um Dinge wie objektorientierte Programmierung zu modellieren, bei der "Objekte" einige versteckte Daten zusammen mit einigen Methoden bündeln, die mit den versteckten Daten arbeiten. So könnte beispielsweise ein Objekt mit zwei Methoden - eine, die eine zurückgibt, Intund eine, die a zurückgibt String- mit diesem Typ implementiert werden:

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

Wie funktioniert das? Das Objekt wird als eine Funktion implementiert, die einige interne Daten vom versteckten Typ enthält a. Um das Objekt tatsächlich zu verwenden, übergeben seine Clients eine "Rückruffunktion", die das Objekt mit den beiden Methoden aufruft. Beispielsweise:

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

Hier rufen wir im Grunde die zweite Methode des Objekts auf, die, deren Typ a → Stringfür ein Unbekanntes ist a. Nun, den myObjectKunden unbekannt ; Diese Clients wissen jedoch anhand der Signatur, dass sie eine der beiden Funktionen darauf anwenden und entweder eine Intoder eine erhalten können String.

Für ein aktuelles Haskell-Beispiel ist unten der Code aufgeführt, den ich geschrieben habe, als ich mich selbst unterrichtet habe RankNTypes. Dies implementiert einen aufgerufenen Typ, ShowBoxder einen Wert eines versteckten Typs zusammen mit seiner ShowKlasseninstanz bündelt . Beachten Sie, dass ich im Beispiel unten eine Liste erstelle, ShowBoxderen erstes Element aus einer Zahl und das zweite aus einer Zeichenfolge besteht. Da die Typen durch die Verwendung der höherrangigen Typen ausgeblendet werden, verstößt dies nicht gegen die Typprüfung.

{-# 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: Für jeden, der dies liest und sich gefragt hat, wie es dazu kommt, dass ExistentialTypesGHC verwendet wird forall, glaube ich, dass der Grund darin liegt, dass diese Art von Technik hinter den Kulissen verwendet wird.

Die Antwort von Luis Casillas gibt viele großartige Informationen darüber, was Rang-2-Typen bedeuten, aber ich werde nur auf einen Punkt eingehen, den er nicht behandelt hat. Wenn ein Argument polymorph sein muss, kann es nicht nur mit mehreren Typen verwendet werden. Es schränkt auch ein, was diese Funktion mit ihren Argumenten tun kann und wie sie ihr Ergebnis erzeugen kann. Das heißt, es gibt dem Anrufer weniger Flexibilität. Warum willst du das tun? Ich beginne mit einem einfachen Beispiel:

Angenommen, wir haben einen Datentyp

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

und wir wollen eine Funktion schreiben

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

Dies erfordert eine Funktion, die eines der Elemente der Liste auswählt und eine IOAktion zurückgibt, mit der Raketen auf dieses Ziel abgefeuert werden. Wir könnten feinen einfachen Typ geben:

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

Das Problem ist, dass wir versehentlich rennen könnten

f (\_ -> BestAlly)

und dann wären wir in großen Schwierigkeiten! Geben feines polymorphen Typs vom Rang 1

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

hilft überhaupt nicht, weil wir den Typ wählen, awenn wir anrufen f, und wir spezialisieren ihn einfach darauf Countryund verwenden unseren bösartigen \_ -> BestAllywieder. Die Lösung besteht darin, einen Typ vom Rang 2 zu verwenden:

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

Jetzt muss die Funktion, die wir übergeben, polymorph sein, also \_ -> BestAllykeine Typprüfung! Tatsächlich wird keine Funktion, die ein Element zurückgibt, das nicht in der angegebenen Liste enthalten ist, typecheck (obwohl einige Funktionen, die in Endlosschleifen gehen oder Fehler erzeugen und daher niemals zurückkehren, dies tun).

Das Obige ist natürlich erfunden, aber eine Variation dieser Technik ist der Schlüssel, um die STMonade sicher zu machen.

Höherrangige Typen sind nicht so exotisch wie die anderen Antworten. Ob Sie es glauben oder nicht, viele objektorientierte Sprachen (einschließlich Java und C #!) Enthalten sie. (Natürlich kennt sie niemand in diesen Gemeinden unter dem beängstigend klingenden Namen "höherrangige Typen".)

Das Beispiel, das ich geben werde, ist eine Lehrbuchimplementierung des Besuchermusters, die ich ständig in meiner täglichen Arbeit verwende. Diese Antwort ist nicht als Einführung in das Besuchermuster gedacht. Dieses Wissen ist an anderer Stelle leicht verfügbar .

In dieser fetten imaginären HR-Anwendung möchten wir Mitarbeiter bearbeiten, die Vollzeit-Festangestellte oder Zeitarbeitskräfte sein können. Meine bevorzugte Variante des Besuchermusters (und tatsächlich diejenige, die für relevant ist RankNTypes) parametrisiert den Rückgabetyp des Besuchers.

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

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

Der Punkt ist, dass eine Reihe von Besuchern mit unterschiedlichen Rückgabetypen alle mit denselben Daten arbeiten können. Dies bedeutet IEmployee, dass keine Meinung darüber Tgeäußert werden darf, was sein sollte.

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);
    }
}

Ich möchte Ihre Aufmerksamkeit auf die Typen lenken. Beachten Sie, dass IEmployeeVisitorder Rückgabetyp universell quantifiziert wird, während IEmployeeer innerhalb seiner AcceptMethode quantifiziert wird, dh auf einem höheren Rang. Klobig von C # nach Haskell übersetzen:

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

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

Da haben Sie es also. Höherrangige Typen werden in C # angezeigt, wenn Sie Typen schreiben, die generische Methoden enthalten.

Folien aus Bryan O'Sullivans Haskell-Kurs in Stanford halfen mir zu verstehen Rank2Types.

Für diejenigen, die mit objektorientierten Sprachen vertraut sind, ist eine höherrangige Funktion einfach eine generische Funktion, die als Argument eine andere generische Funktion erwartet.

ZB in TypeScript könnten Sie schreiben:

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

Sehen Sie, wie der generische Funktionstyp Identifyeine generische Funktion des Typs erfordert Identifier? Dies macht Identifyeine höherrangige Funktion.