¿Cuál es el propósito de Rank2Types?

No soy muy competente en Haskell, por lo que esta podría ser una pregunta muy fácil.

¿Qué limitación de idioma resuelve Rank2Types ? ¿Las funciones en Haskell ya no admiten argumentos polimórficos?

¿Las funciones en Haskell ya no admiten argumentos polimórficos?

Lo hacen, pero solo de rango 1. Esto significa que, si bien puede escribir una función que tome diferentes tipos de argumentos sin esta extensión, no puede escribir una función que use su argumento como diferentes tipos en la misma invocación.

Por ejemplo, la siguiente función no se puede escribir sin esta extensión porque gse usa con diferentes tipos de argumentos en la definición de f:

f g = g 1 + g "lala"

Tenga en cuenta que es perfectamente posible pasar una función polimórfica como argumento a otra función. Entonces, algo así map id ["a","b","c"]es perfectamente legal. Pero la función solo puede usarla como monomórfica. En el ejemplo se mapusa idcomo si tuviera tipo String -> String. Y, por supuesto, también puede pasar una función monomórfica simple del tipo dado en lugar de id. Sin rank2types no hay forma de que una función requiera que su argumento sea una función polimórfica y, por lo tanto, tampoco hay forma de usarla como función polimórfica.

Es difícil entender el polimorfismo de rango superior a menos que estudie el Sistema F directamente, porque Haskell está diseñado para ocultarle los detalles en aras de la simplicidad.

Pero básicamente, la idea aproximada es que los tipos polimórficos realmente no tienen la a -> bforma que tienen en Haskell; en realidad, se ven así, siempre con cuantificadores explícitos:

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

Si no conoce el símbolo "∀", se lee como "para todos"; ∀x.dog(x)significa "para todo x, x es un perro". "Λ" es lambda mayúscula, utilizada para abstraer parámetros de tipo; lo que dice la segunda línea es que id es una función que toma un tipo ty luego devuelve una función que está parametrizada por ese tipo.

Verá, en el Sistema F, no puede simplemente aplicar una función como esa ida un valor de inmediato; primero debe aplicar la función Λ a un tipo para obtener una función λ que aplique a un valor. Así por ejemplo:

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

Haskell estándar (es decir, Haskell 98 y 2010) simplifica esto para usted al no tener ninguno de estos cuantificadores de tipo, lambdas mayúsculas y aplicaciones de tipo, pero detrás de escena GHC los coloca cuando analiza el programa para su compilación. (Todo esto es material en tiempo de compilación, creo, sin sobrecarga de tiempo de ejecución).

Pero el manejo automático de Haskell de esto significa que asume que "∀" nunca aparece en la rama izquierda de un tipo de función ("→"). Rank2Typesy RankNTypesdesactive esas restricciones y le permita anular las reglas predeterminadas de Haskell sobre dónde insertar forall.

Por qué querrías hacer esto? Porque el Sistema F completo y sin restricciones es muy poderoso y puede hacer muchas cosas interesantes. Por ejemplo, la ocultación de tipos y la modularidad se pueden implementar utilizando tipos de rango superior. Tomemos, por ejemplo, una función antigua simple del siguiente tipo de rango 1 (para establecer la escena):

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

Para usar f, la persona que llama primero debe elegir qué tipos usar ry aluego proporcionar un argumento del tipo resultante. Entonces podrías elegir r = Inty a = String:

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

Pero ahora compare eso con el siguiente tipo de rango superior:

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

¿Cómo funciona una función de este tipo? Bueno, para usarlo, primero debes especificar qué tipo usar r. Digamos que elegimos Int:

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

Pero ahora ∀aestá dentro de la flecha de función, por lo que no puede elegir qué tipo usar a; debe aplicar f' Inta una función of del tipo apropiado. Esto significa que la implementación de f'elige qué tipo usar a, no quién llamaf' . Sin tipos de rango superior, por el contrario, la persona que llama siempre elige los tipos.

¿Para qué sirve esto? Bueno, para muchas cosas en realidad, pero una idea es que puede usar esto para modelar cosas como la programación orientada a objetos, donde los "objetos" agrupan algunos datos ocultos junto con algunos métodos que funcionan con los datos ocultos. Entonces, por ejemplo, un objeto con dos métodos, uno que devuelve una Inty otro que devuelve una String, podría implementarse con este tipo:

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

¿Como funciona esto? El objeto se implementa como una función que tiene algunos datos internos de tipo oculto a. Para utilizar realmente el objeto, sus clientes pasan una función de "devolución de llamada" que el objeto llamará con los dos métodos. Por ejemplo:

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

Aquí estamos, básicamente, invocando el segundo método del objeto, aquel cuyo tipo es a → Stringpara un desconocido a. Bueno, desconocido para myObjectlos clientes; pero estos clientes saben, por la firma, que podrán aplicarle cualquiera de las dos funciones y obtener una Into una String.

Para un ejemplo real de Haskell, a continuación se muestra el código que escribí cuando aprendí por mi cuenta RankNTypes. Esto implementa un tipo llamado ShowBoxque agrupa un valor de algún tipo oculto junto con su Showinstancia de clase. Tenga en cuenta que en el ejemplo de la parte inferior, hago una lista de ShowBoxcuyo primer elemento se hizo a partir de un número y el segundo de una cadena. Dado que los tipos están ocultos al usar los tipos de rango superior, esto no viola la verificación de tipos.

{-# 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

PD: para cualquiera que lea esto y se pregunte cómo es que se ExistentialTypesusa GHC forall, creo que la razón es porque está usando este tipo de técnica detrás de escena.

La respuesta de Luis Casillas brinda mucha información excelente sobre lo que significan los tipos de rango 2, pero solo ampliaré un punto que no cubrió. Requerir que un argumento sea polimórfico no solo permite que se use con múltiples tipos; también restringe lo que esa función puede hacer con su (s) argumento (s) y cómo puede producir su resultado. Es decir, le da a la persona que llama menos flexibilidad. ¿Por qué querrías hacer eso? Comenzaré con un ejemplo simple:

Supongamos que tenemos un tipo de datos

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

y queremos escribir una función

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

que toma una función que se supone debe elegir uno de los elementos de la lista que se le da y devolver una IOacción que lanza misiles a ese objetivo. Podríamos dar fun tipo simple:

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

El problema es que podríamos ejecutar accidentalmente

f (\_ -> BestAlly)

¡Y entonces estaríamos en un gran problema! Dar fun tipo polimórfico de rango 1

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

no ayuda en absoluto, porque elegimos el tipo acuando llamamos f, y simplemente lo especializamos Countryy usamos nuestro malware \_ -> BestAllynuevamente. La solución es utilizar un tipo de rango 2:

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

Ahora se requiere que la función que pasamos sea polimórfica, ¡así \_ -> BestAllyque no escribiremos check! De hecho, ninguna función que devuelva un elemento que no esté en la lista que se le da hará una verificación de tipo (aunque algunas funciones que entran en bucles infinitos o producen errores y por lo tanto nunca regresan lo harán).

Lo anterior es artificial, por supuesto, pero una variación de esta técnica es clave para hacer que la STmónada sea segura.

Los tipos de rango superior no son tan exóticos como han demostrado las otras respuestas. Lo crea o no, muchos lenguajes orientados a objetos (¡incluidos Java y C #!) Los incluyen. (Por supuesto, nadie en esas comunidades los conoce por el nombre que suena aterrador "tipos de rango superior").

El ejemplo que voy a dar es una implementación de libro de texto del patrón Visitor, que uso todo el tiempo en mi trabajo diario. Esta respuesta no pretende ser una introducción al patrón de visitantes; que el conocimiento es fácilmente disponible en otros lugares .

En esta fatua aplicación de recursos humanos imaginaria, deseamos operar con empleados que pueden ser empleados permanentes a tiempo completo o contratistas temporales. Mi variante preferida del patrón de visitante (y de hecho la que es relevante para RankNTypes) parametriza el tipo de retorno del visitante.

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

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

El punto es que varios visitantes con diferentes tipos de retorno pueden operar todos con los mismos datos. Este medio no IEmployeedebe expresar ninguna opinión sobre lo que Tdebería ser.

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

Deseo llamar su atención sobre los tipos. Observe que IEmployeeVisitorcuantifica universalmente su tipo de retorno, mientras que lo IEmployeecuantifica dentro de su Acceptmétodo, es decir, en un rango superior. Traduciendo torpemente de C # a Haskell:

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

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

Así que ahí lo tienes. Los tipos de rango superior aparecen en C # cuando escribe tipos que contienen métodos genéricos.

Las diapositivas del curso Haskell de Bryan O'Sullivan en Stanford me ayudaron a entender Rank2Types.

Para aquellos familiarizados con los lenguajes orientados a objetos, una función de rango superior es simplemente una función genérica que espera como argumento otra función genérica.

Por ejemplo, en TypeScript podría escribir:

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

¿Ves cómo el tipo de función genérica Identifyexige una función genérica del tipo Identifier? Esto hace Identifyuna función de rango superior.