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

110

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?

Andrey Shchekin
fuente
Es básicamente una actualización del sistema de tipo HM al cálculo lambda polimórfico también conocido como. λ2 / Sistema F. Tenga en cuenta que la inferencia de tipos es indecidible en λ2.
Poscat

Respuestas:

116

¿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.

sepp2k
fuente
5
Para agregar algunas palabras que conectan mi respuesta con esta: considere la función Haskell f' g x y = g x + g y. Su tipo de rango 1 inferido es forall a r. Num r => (a -> r) -> a -> a -> r. Como forall aestá fuera de las flechas de función, la persona que llama primero debe elegir un tipo para a; si eligen Int, obtenemos f' :: forall r. Num r => (Int -> r) -> Int -> Int -> r, y ahora hemos arreglado el gargumento para que pueda tomar Intpero no String. Si lo habilitamos RankNTypespodemos anotar f'con type forall b c r. Num r => (forall a. a -> r) -> b -> c -> r. Sin embargo, no puedo usarlo, ¿cuál sería g?
Luis Casillas
166

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 = Λtx: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:

tx: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.

Luis Casillas
fuente
2
¡Gracias por una respuesta muy elaborada! (que, por cierto, también finalmente me motivó a aprender la teoría de tipos adecuada y el Sistema F.)
Aleksandar Dimitrov
5
Si tuviera una existspalabra clave, podría definir un tipo existencial como (por ejemplo) data Any = Any (exists a. a), donde Any :: (exists a. a) -> Any. Usando ∀xP (x) → Q ≡ (∃xP (x)) → Q, podemos concluir que Anytambién podría tener un tipo forall a. a -> Anyy de ahí forallproviene la palabra clave. Creo que los tipos existenciales implementados por GHC son solo tipos de datos ordinarios que también contienen todos los diccionarios de clases de tipos requeridos (no pude encontrar una referencia para respaldar esto, lo siento).
Vitus
2
@Vitus: Los existenciales de GHC no están vinculados a los diccionarios de clases de tipos. Puede tener data ApplyBox r = forall a. ApplyBox (a -> r) a; cuando el patrón coincide con ApplyBox f x, obtiene f :: h -> ry x :: hpara un tipo restringido "oculto" h. Si entiendo bien, el caso del diccionario de la clase de tipos se traduce a algo como esto: data ShowBox = forall a. Show a => ShowBox ase traduce a algo como 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
Esa es una gran respuesta a la que tendré que dedicarle un tiempo. Creo que estoy demasiado acostumbrado a las abstracciones que proporcionan los genéricos de C #, por lo que estaba dando mucho de eso por sentado en lugar de comprender realmente la teoría.
Andrey Shchekin
@sacundim: Bueno, "todos los diccionarios de clases de tipos requeridos" también puede significar que no hay ningún diccionario si no lo necesita. :) Mi punto fue que GHC probablemente no codifica tipos existenciales a través de tipos de mayor rango (es decir, la transformación que sugieres - youxP (x) ~ ∀r. (∀xP (x) → r) → r).
Vitus
47

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.

dfeuer
fuente
18

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.

Benjamin Hodgson
fuente
1
Me gustaría saber si alguien más ha escrito sobre el soporte de C # / Java / Blub para tipos de rango superior. Si usted, querido lector, conoce alguno de estos recursos, por favor envíelos a mi manera.
Benjamin Hodgson
-2

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.

Asad Saeeduddin
fuente
¿Qué agrega esto a la respuesta de sepp2k?
dfeuer
¿O de Benjamin Hodgson, en realidad?
dfeuer
1
Creo que te perdiste el punto de Hodgson. Accepttiene un tipo polimórfico de rango 1, pero es un método de IEmployee, que es en sí mismo rango 2. Si alguien me da un IEmployee, puedo abrirlo y usar su Acceptmétodo en cualquier tipo.
Dfeuer
1
Su ejemplo también es de rango 2, a través de la Visiteeclase que presenta. Una función f :: Visitee e => T ees (una vez desazucarado el material de la clase) esencialmente f :: (forall r. e -> Visitor e r -> r) -> T e. Haskell 2010 te permite salirte con la tuya con un polimorfismo de rango 2 limitado usando clases como esa.
dfeuer
1
No se puede flotar forallen mi ejemplo. No tengo una referencia a mano, pero es posible que encuentre algo en "Elimine sus clases de tipos" . El polimorfismo de rango superior puede introducir problemas de verificación de tipos, pero el tipo limitado implícito en el sistema de clases está bien.
dfeuer