Qual è lo scopo di Rank2Types?

Non sono molto abile in Haskell, quindi questa potrebbe essere una domanda molto facile.

Quali limitazioni linguistiche risolvono Rank2Types ? Le funzioni in Haskell non supportano già argomenti polimorfici?

Le funzioni in Haskell non supportano già argomenti polimorfici?

Lo fanno, ma solo di rango 1. Ciò significa che mentre è ansible scrivere una funzione che accetta diversi tipi di argomenti senza questa estensione, non è ansible scrivere una funzione che utilizza il suo argomento come tipi diversi nella stessa invocazione.

Ad esempio, la seguente funzione non può essere digitata senza questa estensione perché g è usato con diversi tipi di argomenti nella definizione di f :

 fg = g 1 + g "lala" 

Si noti che è perfettamente ansible passare una funzione polimorfica come argomento a un’altra funzione. Quindi qualcosa come map id ["a","b","c"] è perfettamente legale. Ma la funzione può solo usarlo come monomorfico. Nella map esempio usa id come se avesse tipo String -> String . E ovviamente puoi anche passare una semplice funzione monomorfica del tipo dato invece di id . Senza rank2types non è ansible che una funzione richieda che il suo argomento debba essere una funzione polimorfica e quindi anche nessun modo di usarlo come funzione polimorfica.

È difficile capire il polimorfismo di rango superiore a meno che non studi direttamente il sistema F , perché Haskell è progettato per hide i dettagli di ciò da te nell’interesse della semplicità.

Ma fondamentalmente, l’idea approssimativa è che i tipi polimorfici non hanno realmente il formato a -> b che fanno in Haskell; in realtà, assomigliano a questo, sempre con quantificatori espliciti:

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

Se non conosci il simbolo “∀”, viene letto come “per tutti”; ∀x.dog(x) significa “per tutti x, x è un cane”. “Λ” è il capitale lambda, utilizzato per l’astrazione su parametri di tipo; quello che la seconda riga dice è che id è una funzione che accetta un tipo t , e quindi restituisce una funzione parametrizzata da quel tipo.

Vedete, in System F, non potete semplicemente applicare una funzione come quella id ad un valore immediatamente; per prima cosa è necessario applicare la funzione to a un tipo per ottenere una funzione λ che si applica a un valore. Quindi per esempio:

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

Haskell standard (ad esempio, Haskell 98 e 2010) semplifica questo per voi non avendo nessuno di questi quantificatori di tipo, lambda di capitale e applicazioni di tipo, ma dietro le quinte GHC li inserisce quando analizza il programma per la compilazione. (Questa è tutta roba compilabile, credo, senza sovraccarico di runtime.)

Ma la gestione automatica di Haskell di questo significa che presuppone che “∀” non appaia mai sul ramo di sinistra di un tipo di funzione (“→”). Rank2Types e RankNTypes distriggersno tali restrizioni e consentono di ignorare le regole predefinite di Haskell per dove inserire forall .

Perché vorresti farlo? Perché il sistema F completo e senza restrizioni è potente, e può fare un sacco di cose interessanti. Ad esempio, è ansible implementare il tipo di occultamento e modularità utilizzando i tipi di rango più elevato. Prendiamo ad esempio una semplice vecchia funzione del seguente tipo di rank-1 (per impostare la scena):

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

Per usare f , il chiamante deve prima scegliere quali tipi usare per r e a , quindi fornire un argomento del tipo risultante. Quindi puoi scegliere r = Int e a = String :

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

Ma ora confrontalo con il seguente tipo di rango più alto:

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

Come funziona una funzione di questo tipo? Bene, per usarlo, prima si specifica quale tipo usare per r . Diciamo che selezioniamo Int :

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

Ma ora il ∀a trova all’interno della freccia della funzione, quindi non puoi scegliere quale tipo usare per a ; devi applicare f' Int a una Λ-funzione del tipo appropriato. Ciò significa che l’implementazione di f' arriva a scegliere quale tipo usare per a , non il chiamante di f' . Senza tipi di rango superiore, al contrario, il chiamante sceglie sempre i tipi.

A cosa serve questo? Bene, per molte cose in realtà, ma un’idea è che si può usare questo per modellare cose come la programmazione orientata agli oggetti, dove “oggetti” raggruppano alcuni dati nascosti insieme ad alcuni metodi che funzionano sui dati nascosti. Ad esempio, un object con due metodi, uno che restituisce un Int e un altro che restituisce una String , potrebbe essere implementato con questo tipo:

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

Come funziona? L’object è implementato come una funzione che ha alcuni dati interni di tipo nascosto a . Per utilizzare effettivamente l’object, i suoi client passano in una funzione di “callback” che l’object chiamerà con i due metodi. Per esempio:

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

Qui, in pratica, invochiamo il secondo metodo dell’object, quello il cui tipo è a → String per uno sconosciuto a . Beh, sconosciuto ai myObject di myObject ; ma questi client sanno, dalla firma, che saranno in grado di applicare una delle due funzioni e ottenere un Int o una String .

Per un vero esempio di Haskell, di seguito è riportato il codice che ho scritto quando ho insegnato a me stesso RankNTypes . Questo implementa un tipo chiamato ShowBox che raggruppa insieme un valore di un tipo nascosto insieme alla sua istanza di class Show . Si noti che nell’esempio in basso, ShowBox un elenco di ShowBox cui primo elemento è stato creato da un numero e il secondo da una stringa. Poiché i tipi sono nascosti utilizzando i tipi di rango più elevato, questo non viola il controllo dei tipi.

 {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ImpredicativeTypes #-} type ShowBox = forall b. (forall a. Show a => a -> b) -> b mkShowBox :: Show a => a -> ShowBox mkShowBox x = \k -> kx -- | 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: per chiunque stia leggendo questo che si è chiesto come mai ExistentialTypes in GHC usa forall , credo che la ragione sia perché sta usando questo tipo di tecnica dietro le quinte.

La risposta di Luis Casillas fornisce moltissime informazioni su cosa significano due tipi di rango, ma mi limiterò ad ampliare un punto che non ha coperto. Richiedere un argomento per essere polimorfico non consente solo di utilizzarlo con più tipi; limita anche ciò che questa funzione può fare con i suoi argomenti e come può produrre il suo risultato. Cioè, dà al chiamante meno flessibilità. Perché vorresti farlo? Inizierò con un semplice esempio:

Supponiamo di avere un tipo di dati

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

e vogliamo scrivere una funzione

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

che prende una funzione che dovrebbe scegliere uno degli elementi della lista che è dato e restituire un missile di lancio di azione IO su quell’objective. Potremmo dare a un tipo semplice:

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

Il problema è che potremmo correre accidentalmente

 f (\_ -> BestAlly) 

e poi saremmo in grossi guai! Fornire un tipo polimorfo di rango 1

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

non aiuta affatto, perché scegliamo il tipo a quando chiamiamo f , e lo specializziamo solo in Country e usiamo ancora il nostro malizioso \_ -> BestAlly . La soluzione è usare un tipo di grado 2:

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

Ora la funzione che passiamo deve essere polimorfa, quindi \_ -> BestAlly non scriverà check! In effetti, nessuna funzione che restituisce un elemento non presente nell’elenco viene digitata tipograficamente (sebbene alcune funzioni che vanno in loop infiniti o producano errori e quindi non ritornino mai lo faranno).

Quanto sopra è inventato, ovviamente, ma una variazione su questa tecnica è la chiave per rendere sicura la monade ST .

I tipi di rango più elevato non sono così esotici come hanno fatto le altre risposte. Che ci crediate o no, molti linguaggi orientati agli oggetti (incluso Java e C #!) Li caratterizzano. (Naturalmente, nessuno in quelle comunità li conosce con il nome spaventoso di “tipi più alti”.)

L’esempio che darò è un’attuazione da manuale del pattern Visitor, che uso sempre nel mio lavoro quotidiano. Questa risposta non è intesa come introduzione al modello del visitatore; quella conoscenza è facilmente disponibile altrove .

In questa fatua applicazione delle risorse umane immaginarie, desideriamo operare su dipendenti che possono essere impiegati permanenti a tempo pieno o appaltatori temporanei. La mia variante preferita del pattern Visitor (e in effetti quella che è rilevante per RankNTypes ) parametrizza il tipo di ritorno del visitatore.

 interface IEmployeeVisitor { T Visit(PermanentEmployee e); T Visit(Contractor c); } class XmlVisitor : IEmployeeVisitor { /* ... */ } class PaymentCalculator : IEmployeeVisitor { /* ... */ } 

Il punto è che un numero di visitatori con diversi tipi di ritorno può operare tutti sugli stessi dati. Ciò significa che IEmployee deve esprimere alcuna opinione su cosa T dovrebbe essere.

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

Desidero attirare la vostra attenzione sui tipi. Si osservi che IEmployeeVisitor quantifica universalmente il suo tipo restituito, mentre IEmployee quantifica nel suo metodo Accept , cioè in una posizione più alta. Traducendo clunkily da C # a Haskell:

 data IEmployeeVisitor r = IEmployeeVisitor { visitPermanent :: PermanentEmployee -> r, visitContractor :: Contractor -> r } newtype IEmployee = IEmployee { accept :: forall r. IEmployeeVisitor r -> r } 

Così il gioco è fatto. I tipi di rango più elevato vengono visualizzati in C # quando si scrivono tipi contenenti metodi generici.

Gli Rank2Types del corso Haskell di Stanford di Bryan O’Sullivan mi hanno aiutato a capire Rank2Types .

Per chi ha familiarità con i linguaggi orientati agli oggetti, una funzione di rango più elevato è semplicemente una funzione generica che si aspetta come argomento un’altra funzione generica.

Ad esempio in TypeScript è ansible scrivere:

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

Vedi come il tipo di funzione generica Identify richiede una funzione generica del tipo Identifier ? Questo rende Identify una funzione di livello più alto.