Quel est le but de Rank2Types?

110

Je ne maîtrise pas vraiment Haskell, c'est peut-être une question très simple.

Quelles sont les limitations linguistiques résolues par Rank2Types ? Les fonctions dans Haskell ne prennent-elles pas déjà en charge les arguments polymorphes?

Andrey Shchekin
la source
Il s'agit essentiellement d'une mise à niveau du système de type HM vers le calcul lambda polymorphe aka. λ2 / Système F. Gardez à l'esprit que l'inférence de type est indécidable dans λ2.
Poscat le

Réponses:

116

Les fonctions de Haskell ne prennent-elles pas déjà en charge les arguments polymorphes?

Ils le font, mais seulement de rang 1. Cela signifie que si vous pouvez écrire une fonction qui prend différents types d'arguments sans cette extension, vous ne pouvez pas écrire une fonction qui utilise son argument comme différents types dans la même invocation.

Par exemple, la fonction suivante ne peut pas être tapée sans cette extension car elle gest utilisée avec différents types d'arguments dans la définition de f:

f g = g 1 + g "lala"

Notez qu'il est parfaitement possible de passer une fonction polymorphe comme argument à une autre fonction. Donc, quelque chose comme map id ["a","b","c"]est parfaitement légal. Mais la fonction ne peut l'utiliser que comme monomorphe. Dans l'exemple, maputilise idcomme s'il avait du type String -> String. Et bien sûr, vous pouvez également passer une simple fonction monomorphe du type donné à la place de id. Sans rank2types, il n'y a aucun moyen pour une fonction d'exiger que son argument soit une fonction polymorphe et donc également aucun moyen de l'utiliser comme fonction polymorphe.

sepp2k
la source
5
Pour ajouter quelques mots reliant ma réponse à celle-ci: considérez la fonction Haskell f' g x y = g x + g y. Son type de rang 1 inféré est forall a r. Num r => (a -> r) -> a -> a -> r. Puisqu'il se forall atrouve en dehors des flèches de fonction, l'appelant doit d'abord choisir un type pour a; s'ils choisissent Int, nous obtenons f' :: forall r. Num r => (Int -> r) -> Int -> Int -> r, et maintenant nous avons corrigé l' gargument afin qu'il puisse prendre Intmais pas String. Si nous activons, RankNTypesnous pouvons annoter f'avec le type forall b c r. Num r => (forall a. a -> r) -> b -> c -> r. Je ne peux pas l'utiliser, cependant - que serait-ce g?
Luis Casillas
166

Il est difficile de comprendre le polymorphisme de rang supérieur à moins d'étudier directement le système F , car Haskell est conçu pour vous en cacher les détails dans un souci de simplicité.

Mais fondamentalement, l'idée approximative est que les types polymorphes n'ont pas vraiment la a -> bforme qu'ils ont dans Haskell; en réalité, ils ressemblent à ceci, toujours avec des quantificateurs explicites:

id :: a.a  a
id = Λtx:t.x

Si vous ne connaissez pas le symbole "∀", il est lu comme "pour tous"; ∀x.dog(x)signifie "pour tout x, x est un chien." "Λ" est un lambda majuscule, utilisé pour l'abstraction des paramètres de type; ce que dit la deuxième ligne, c'est que id est une fonction qui prend un type t, puis retourne une fonction paramétrée par ce type.

Vous voyez, dans le système F, vous ne pouvez pas simplement appliquer une fonction comme celle-là idà une valeur tout de suite; vous devez d'abord appliquer la fonction Λ à un type afin d'obtenir une fonction λ que vous appliquez à une valeur. Donc par exemple:

tx:t.x) Int 5 = x:Int.x) 5
                  = 5

Standard Haskell (c'est-à-dire, Haskell 98 et 2010) simplifie cela pour vous en n'ayant aucun de ces quantificateurs de type, lambdas majuscules et applications de type, mais dans les coulisses, GHC les place lorsqu'il analyse le programme pour la compilation. (Ce sont tous des trucs de compilation, je crois, sans surcharge d'exécution.)

Mais la gestion automatique de cela par Haskell signifie qu'elle suppose que "∀" n'apparaît jamais sur la branche gauche d'une fonction ("→") de type. Rank2Typeset RankNTypesdésactivez ces restrictions et vous permettre de remplacer les règles par défaut de Haskell pour savoir où insérer forall.

Pourquoi voudriez-vous faire ça? Parce que le système F complet et sans restriction est extrêmement puissant et peut faire beaucoup de choses intéressantes. Par exemple, le masquage de type et la modularité peuvent être implémentés à l'aide de types de rang supérieur. Prenons par exemple une ancienne fonction simple du type de rang 1 suivant (pour définir la scène):

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

Pour utiliser f, l'appelant doit d' abord choisir les types à utiliser pour ret a, puis fournir un argument du type résultant. Vous pouvez donc choisir r = Intet a = String:

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

Mais comparez maintenant cela au type de rang supérieur suivant:

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

Comment fonctionne une fonction de ce type? Eh bien, pour l'utiliser, spécifiez d'abord le type à utiliser r. Disons que nous choisissons Int:

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

Mais maintenant, le ∀aest à l' intérieur de la flèche de fonction, vous ne pouvez donc pas choisir le type à utiliser a; vous devez postuler f' Intà une fonction Λ du type approprié. Cela signifie que l'implémentation de f'permet de choisir le type à utiliser a, pas l'appelant def' . Sans types de rang supérieur, au contraire, l'appelant choisit toujours les types.

À quoi cela sert-il? Eh bien, pour beaucoup de choses en fait, mais une idée est que vous pouvez l'utiliser pour modéliser des choses comme la programmation orientée objet, où les "objets" regroupent des données cachées avec des méthodes qui fonctionnent sur les données cachées. Ainsi, par exemple, un objet avec deux méthodes - une qui renvoie an Intet un autre qui renvoie a String, pourrait être implémenté avec ce type:

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

Comment cela marche-t-il? L'objet est implémenté comme une fonction qui a des données internes de type caché a. Pour utiliser réellement l'objet, ses clients passent une fonction de "callback" que l'objet appellera avec les deux méthodes. Par exemple:

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

Ici, nous invoquons essentiellement la deuxième méthode de l'objet, celle dont le type est a → Stringpour une inconnue a. Eh bien, inconnu myObjectdes clients de; mais ces clients savent, d'après la signature, qu'ils pourront lui appliquer l'une ou l'autre des deux fonctions et obtenir soit un Intsoit un String.

Pour un exemple réel de Haskell, vous trouverez ci-dessous le code que j'ai écrit lorsque j'ai appris moi-même RankNTypes. Cela implémente un type appelé ShowBoxqui regroupe une valeur d'un type caché avec son Showinstance de classe. Notez que dans l'exemple en bas, je fais une liste ShowBoxdont le premier élément a été fait à partir d'un nombre, et le second d'une chaîne. Étant donné que les types sont masqués à l'aide des types de rang supérieur, cela ne viole pas la vérification de type.

{-# 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: pour quiconque lit ceci et se demande comment se fait l' ExistentialTypesutilisation du GHC forall, je pense que la raison en est qu'il utilise ce genre de technique en coulisses.

Luis Casillas
la source
2
Merci pour une réponse très élaborée! (ce qui, d'ailleurs, m'a aussi finalement motivé à apprendre la théorie des types appropriée et le système F.)
Aleksandar Dimitrov
5
Si vous aviez un existsmot-clé, vous pourriez définir un type existentiel comme (par exemple) data Any = Any (exists a. a), où Any :: (exists a. a) -> Any. En utilisant ∀xP (x) → Q ≡ (∃xP (x)) → Q, nous pouvons conclure que cela Anypourrait aussi avoir un type forall a. a -> Anyet c'est de là que forallvient le mot - clé. Je crois que les types existentiels tels qu'implémentés par GHC ne sont que des types de données ordinaires qui portent également tous les dictionnaires de classes de types requis (je n'ai pas trouvé de référence pour le sauvegarder, désolé).
Vitus
2
@Vitus: les existentiels GHC ne sont pas liés aux dictionnaires de classes de types. Vous pouvez avoir data ApplyBox r = forall a. ApplyBox (a -> r) a; lorsque vous correspondez à un motif ApplyBox f x, vous obtenez f :: h -> ret x :: hpour un type restreint "masqué" h. Si je comprends bien, le cas du dictionnaire de classes de types est traduit en quelque chose comme ceci: data ShowBox = forall a. Show a => ShowBox aest traduit en quelque chose comme 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
C'est une excellente réponse sur laquelle je devrai passer du temps. Je pense que je suis trop habitué aux abstractions fournies par les génériques C #, donc je prenais beaucoup de cela pour acquis au lieu de comprendre la théorie.
Andrey Shchekin
@sacundim: Eh bien, "tous les dictionnaires de classes de types requis" peut également signifier aucun dictionnaire si vous n'en avez pas besoin. :) Ce que je veux dire, c'est que GHC n'encode probablement pas les types existentiels via des types de rang supérieur (c'est-à-dire la transformation que vous suggérez - ∃xP (x) ~ ∀r. (∀xP (x) → r) → r).
Vitus
47

La réponse de Luis Casillas donne beaucoup d'informations sur ce que signifient les types de rang 2, mais je vais simplement développer un point qu'il n'a pas couvert. Exiger qu'un argument soit polymorphe ne lui permet pas seulement d'être utilisé avec plusieurs types; il restreint également ce que cette fonction peut faire avec ses arguments et comment elle peut produire son résultat. Autrement dit, cela donne moins de flexibilité à l'appelant . Pourquoi voudriez-vous faire ça? Je vais commencer par un exemple simple:

Supposons que nous ayons un type de données

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

et nous voulons écrire une fonction

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

qui prend une fonction qui est censée choisir l'un des éléments de la liste qui lui est donnée et renvoyer une IOaction lançant des missiles sur cette cible. Nous pourrions donner fun type simple:

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

Le problème est que nous pourrions courir accidentellement

f (\_ -> BestAlly)

et alors nous aurions de gros ennuis! Donnantf un type polymorphe de rang 1

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

n'aide pas du tout, car nous choisissons le type alorsque nous appelons f, et nous le spécialisons simplement Countryet utilisons notre\_ -> BestAlly nouveau . La solution est d'utiliser un type de rang 2:

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

Maintenant, la fonction que nous transmettons doit être polymorphe, donc \_ -> BestAlly ne tapez pas check! En fait, aucune fonction retournant un élément ne figurant pas dans la liste qui lui est donnée ne sera typé (bien que certaines fonctions qui entrent dans des boucles infinies ou produisent des erreurs et donc ne reviennent jamais le feront).

Ce qui précède est artificiel, bien sûr, mais une variante de cette technique est essentielle pour STsécuriser la monade.

dfeuer
la source
18

Les types de rang plus élevé ne sont pas aussi exotiques que les autres réponses l'ont laissé entendre. Croyez-le ou non, de nombreux langages orientés objet (y compris Java et C #!) Les intègrent. (Bien sûr, personne dans ces communautés ne les connaît sous le nom effrayant de "types de rang supérieur".)

L'exemple que je vais donner est une implémentation classique du modèle Visiteur, que j'utilise tout le temps dans mon travail quotidien. Cette réponse ne se veut pas une introduction au modèle de visiteur; cette connaissance est facilement disponible ailleurs .

Dans cette folle application RH imaginaire, nous souhaitons opérer sur des salariés qui peuvent être permanents à temps plein ou intérimaires. Ma variante préférée du modèle de visiteur (et en fait celle qui est pertinente pour RankNTypes) paramètre le type de retour du visiteur.

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

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

Le fait est qu'un certain nombre de visiteurs avec des types de retour différents peuvent tous opérer sur les mêmes données. Ce moyen ne IEmployeedoit exprimer aucune opinion sur ce qui Tdevrait être.

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

Je souhaite attirer votre attention sur les types. Observez que IEmployeeVisitorquantifie universellement son type de retour, alors que le IEmployeequantifie à l'intérieur de sa Acceptméthode - c'est-à-dire à un rang supérieur. Traduire maladroitement de C # à Haskell:

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

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

Alors là vous l'avez. Les types de rang supérieur apparaissent en C # lorsque vous écrivez des types contenant des méthodes génériques.

Benjamin Hodgson
la source
1
J'aimerais savoir si quelqu'un d'autre a écrit sur le support de C # / Java / Blub pour les types de rang plus élevé. Si vous, cher lecteur, connaissez de telles ressources, envoyez-les moi!
Benjamin Hodgson
-2

Pour ceux qui sont familiers avec les langages orientés objet, une fonction de rang supérieur est simplement une fonction générique qui attend comme argument une autre fonction générique.

Par exemple, dans TypeScript, vous pouvez écrire:

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

Voyez comment le type de fonction générique Identifyexige une fonction générique du type Identifier? Cela fait Identifyune fonction de rang supérieur.

Asad Saeeduddin
la source
Qu'est-ce que cela ajoute à la réponse de sepp2k?
dfeuer le
Ou de Benjamin Hodgson, d'ailleurs?
dfeuer le
1
Je pense que vous avez manqué le point de Hodgson. Accepta un type polymorphe de rang 1, mais c'est une méthode de IEmployee, qui est elle-même de rang 2. Si quelqu'un me donne un IEmployee, je peux l'ouvrir et utiliser sa Acceptméthode à n'importe quel type.
dfeuer le
1
Votre exemple est également de rang 2, par le biais de la Visiteeclasse que vous introduisez. Une fonction f :: Visitee e => T eest (une fois que le truc de la classe est désucré) essentiellement f :: (forall r. e -> Visitor e r -> r) -> T e. Haskell 2010 vous permet de vous en sortir avec un polymorphisme de rang 2 limité en utilisant des classes comme ça.
dfeuer le
1
Vous ne pouvez pas flotter foralldans mon exemple. Je n'ai pas de référence, mais vous trouverez peut-être quelque chose dans "Scrap Your Type Classes" . Le polymorphisme de rang supérieur peut en effet introduire des problèmes de vérification de type, mais le tri limité implicite dans le système de classes est très bien.
dfeuer le