Qual é a finalidade do Rank2Types?

Não sou muito proficiente em Haskell, então essa pode ser uma pergunta muito fácil.

Que limitação de idioma o Rank2Types resolve? As funções em Haskell já não suportam argumentos polimórficos?

As funções em Haskell já não suportam argumentos polimórficos?

Eles fazem isso, mas apenas na classificação 1. Isso significa que, embora você possa escrever uma função que receba diferentes tipos de argumentos sem essa extensão, não pode escrever uma função que use seu argumento como tipos diferentes na mesma invocação.

Por exemplo, a seguinte função não pode ser digitada sem esta extensão porque gé usada com diferentes tipos de argumento na definição de f:

f g = g 1 + g "lala"

Observe que é perfeitamente possível passar uma função polimórfica como um argumento para outra função. Portanto, algo como map id ["a","b","c"]é perfeitamente legal. Mas a função só pode usá-lo como monomórfico. No exemplo mapusa idcomo se tivesse tipo String -> String. E, claro, você também pode passar uma função monomórfica simples do tipo fornecido em vez de id. Sem rank2types, não há como uma função exigir que seu argumento seja uma função polimórfica e, portanto, também não há como usá-lo como uma função polimórfica.

É difícil entender o polimorfismo de classificação superior, a menos que você estude o Sistema F diretamente, porque Haskell foi projetado para esconder de você os detalhes no interesse da simplicidade.

Mas basicamente, a ideia geral é que os tipos polimórficos não têm realmente a a -> bforma que têm em Haskell; na realidade, são assim, sempre com quantificadores explícitos:

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

Se você não souber o símbolo "∀", ele será lido como "para todos"; ∀x.dog(x)significa "para todo x, x é um cachorro". "Λ" é lambda maiúsculo, usado para abstrair os parâmetros de tipo; o que a segunda linha diz é que id é uma função que recebe um tipo te, em seguida, retorna uma função parametrizada por esse tipo.

Veja, no Sistema F, você não pode simplesmente aplicar uma função como essa ida um valor imediatamente; primeiro você precisa aplicar a função Λ a um tipo para obter uma função λ que você aplica a um valor. Então, por exemplo:

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

Haskell padrão (ou seja, Haskell 98 e 2010) simplifica isso para você por não ter nenhum desses quantificadores de tipo, lambdas capitais e aplicativos de tipo, mas nos bastidores o GHC os coloca quando analisa o programa para compilação. (Isso é tudo em tempo de compilação, eu acredito, sem sobrecarga de tempo de execução.)

Mas o tratamento automático de Haskell significa que ele assume que "∀" nunca aparece no ramo esquerdo de um tipo de função ("→"). Rank2Typese RankNTypesdesative essas restrições e permita que você substitua as regras padrão de Haskell para onde inserir forall.

Por que você quer fazer isso? Porque o System F completo e irrestrito é muito poderoso e pode fazer muitas coisas legais. Por exemplo, ocultação de tipo e modularidade podem ser implementadas usando tipos de classificação superior. Tome por exemplo uma função simples e antiga do seguinte tipo de classificação 1 (para definir o cenário):

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

Para usar f, o chamador primeiro deve escolher quais tipos usar para re a, em seguida, fornecer um argumento do tipo resultante. Então você pode escolher r = Inte a = String:

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

Mas agora compare isso com o seguinte tipo de classificação superior:

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

Como funciona uma função desse tipo? Bem, para usá-lo, primeiro você especifica para qual tipo usar r. Digamos que escolhemos Int:

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

Mas agora ∀aestá dentro da seta de função, então você não pode escolher que tipo usar a; você deve aplicar f' Inta uma função Λ do tipo apropriado. Isso significa que a implementação de f'consegue escolher o tipo de uso a, não o chamador def' . Sem tipos de classificação superior, ao contrário, o chamador sempre escolhe os tipos.

Para que isso é útil? Bem, para muitas coisas, na verdade, mas uma ideia é que você pode usar isso para modelar coisas como programação orientada a objetos, onde "objetos" empacotam alguns dados ocultos junto com alguns métodos que funcionam nos dados ocultos. Portanto, por exemplo, um objeto com dois métodos - um que retorna um Inte outro que retorna a String, pode ser implementado com este tipo:

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

Como é que isso funciona? O objeto é implementado como uma função que possui alguns dados internos de tipo oculto a. Para realmente usar o objeto, seus clientes passam uma função de "retorno de chamada" que o objeto chamará com os dois métodos. Por exemplo:

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

Aqui estamos, basicamente, invocando o segundo método do objeto, aquele cujo tipo é a → Stringpara um desconhecido a. Bem, desconhecido para myObjectos clientes de; mas esses clientes sabem, pela assinatura, que poderão aplicar qualquer uma das duas funções a ela e obter um Intou a String.

Para um exemplo real de Haskell, abaixo está o código que escrevi quando aprendi sozinho RankNTypes. Isso implementa um tipo chamado ShowBoxque agrupa um valor de algum tipo oculto junto com sua Showinstância de classe. Observe que no exemplo abaixo, faço uma lista de ShowBoxcujo primeiro elemento foi feito de um número e o segundo de uma string. Uma vez que os tipos são ocultados usando os tipos de classificação superior, isso não viola a verificação de tipo.

{-# 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: para quem está lendo isso e quer saber como o ExistentialTypesGHC usa forall, acredito que a razão é porque ele está usando esse tipo de técnica nos bastidores.

A resposta de Luis Casillas fornece muitas informações excelentes sobre o que significam os tipos de classificação 2, mas vou apenas expandir um ponto que ele não cobriu. Exigir que um argumento seja polimórfico não permite apenas que ele seja usado com vários tipos; também restringe o que aquela função pode fazer com seu (s) argumento (s) e como pode produzir seu resultado. Ou seja, dá menos ao chamador flexibilidade . Por que você gostaria de fazer isso? Vou começar com um exemplo simples:

Suponha que temos um tipo de dados

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

e queremos escrever uma função

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

que assume uma função que deve escolher um dos elementos da lista fornecida e retornar uma IOação de lançamento de mísseis naquele alvo. Poderíamos dar fum tipo simples:

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

O problema é que podemos executar acidentalmente

f (\_ -> BestAlly)

e então estaríamos em apuros! Dando fum tipo polimórfico de classificação 1

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

não ajuda em nada, porque escolhemos o tipo aquando ligamos f, e apenas nos especializamos Countrye usamos o nosso malicioso \_ -> BestAllynovamente. A solução é usar um tipo de classificação 2:

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

Agora, a função que passamos deve ser polimórfica, portanto \_ -> BestAlly, não digite check! Na verdade, nenhuma função que retorne um elemento que não esteja na lista fornecida irá typecheck (embora algumas funções que entram em loops infinitos ou produzam erros e, portanto, nunca retornem o farão).

O que foi dito acima é planejado, é claro, mas uma variação dessa técnica é a chave para tornar a STmônada segura.

Os tipos de classificação mais alta não são tão exóticos quanto as outras respostas parecem. Acredite ou não, muitas linguagens orientadas a objetos (incluindo Java e C #!) Os apresentam. (Claro, ninguém nessas comunidades os conhece pelo nome assustador de "tipos de classificação superior".)

O exemplo que vou dar é uma implementação de livro do padrão Visitor, que uso o tempo todo em meu trabalho diário. Esta resposta não pretende ser uma introdução ao padrão do visitante; esse conhecimento está prontamente disponível em outro lugar .

Nesta aplicação de RH imaginária idiota, desejamos operar com funcionários que podem ser funcionários permanentes em tempo integral ou contratados temporários. Minha variante preferida do padrão Visitor (e de fato aquela que é relevante RankNTypes) parametriza o tipo de retorno do visitante.

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

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

A questão é que vários visitantes com diferentes tipos de retorno podem operar com os mesmos dados. Este meio não IEmployeedeve expressar nenhuma opinião sobre o que Tdeveria 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);
    }
}

Desejo chamar sua atenção para os tipos. Observe que IEmployeeVisitorquantifica universalmente seu tipo de retorno, enquanto IEmployeequantifica-o dentro de seu Acceptmétodo - ou seja, em um posto superior. Traduzindo desajeitadamente de C # para Haskell:

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

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

Então aí está. Tipos de classificação superior aparecem em C # quando você escreve tipos que contêm métodos genéricos.

Os slides do curso Haskell de Bryan O'Sullivan em Stanford me ajudaram a entender Rank2Types.

Para aqueles familiarizados com as linguagens orientadas a objetos, uma função de classificação superior é simplesmente uma função genérica que espera como seu argumento outra função genérica.

Por exemplo, em TypeScript você pode escrever:

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

Veja como o tipo de função genérica Identifyexige uma função genérica do tipo Identifier? Isso torna Identifyuma função de classificação superior.