Quel est le but de Rank2Types?

Question

Je ne maîtrise pas très bien Haskell, alors la question pourrait être très facile.

Quelle limitation de langue résolus par Rank2Types ?
Les fonctions de Haskell ne prennent-elles déjà en charge les arguments polymorphes?

Answer 1

Il est difficile de comprendre de plus haut rang polymorphisme, à moins que vous étude le Système F directement, parce que Haskell est conçu pour cacher les détails de qui de vous, dans l'intérêt de la simplicité.

Mais, fondamentalement, l'idée est que les types polymorphes n'ont pas vraiment de l' a -> b formulaire qu'ils n'en Haskell; en réalité, ils ressemblent à de ce, toujours de manière explicite les quantificateurs:

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

Si vous ne connaissez pas le "∀" symbole, c'est de lire que "pour tous"; ∀x.dog(x) signifie "pour tout x, x est un chien." "Λ", c'est le capital lambda, utilisées pour le captage sur les paramètres de type; ce que la deuxième ligne indique que l'id est une fonction qui prend un type t, puis retourne une fonction qui est paramétrée par le type.

Vous voyez, dans le Système F, vous ne pouvez pas appliquer une fonction comme ça id la valeur immédiatement; vous devez d'abord appliquer le Λ-fonction d'un type afin d'obtenir un λ-fonction que vous appliquez à une valeur. Ainsi, par exemple:

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

Standard Haskell (c'est à dire, Haskell 98 et 2010) simplifie pour vous en n'ayant aucun de ces types de quantificateurs, capitale des lambdas et les applications de type, mais en coulisses, le GHC met quand il analyse le programme pour la compilation. (C'est tout au moment de la compilation de trucs, je crois, pas de gestion d'exécution.)

Mais Haskell manipulation automatique, cela signifie qu'il suppose que "∀" n'apparaît jamais sur la gauche de la branche d'une fonction ("→") de type. Rank2Types et RankNTypes désactiver ces restrictions et vous permettent de remplacer Haskell des règles par défaut pour l'endroit où insérer forall.

Pourquoi voudriez-vous faire cela? Parce que le plein, sans restriction de F est hella puissant, et il peut faire beaucoup de trucs cool. Par exemple, le type de la clandestinité et de la modularité peut être mis en œuvre à l'aide de rang supérieur à partir de types. Prenez par exemple un simple vieux de la fonction du rang suivant-1 de type (de la scène):

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

Pour utiliser f, l'appelant doit d'abord choisir les types à utiliser pour l' r et a, puis fournir un argument de type résultant. Si vous avez pu récupérer r = Int et a = String:

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

Mais maintenant, comparez cela à la suite de plus haut rang de type:

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

Comment fonctionne une fonction de ce type de travail? Ainsi, pour l'utiliser, il faut d'abord spécifier le type à utiliser pour l' r. Dites-nous prendre en Int:

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

Mais maintenant, l' ∀a est à l'intérieur de la fonction de la flèche, de sorte que vous ne pouvez pas choisir ce type à utiliser pour l' a; vous devez demander l' f' Int pour un Λ-fonction du type approprié. Cela signifie que la mise en œuvre de l' f' obtient à choisir ce type à utiliser pour l' a, pas l'appelant de f'. Sans de plus haut rang types, au contraire, l'appelant choisit toujours les types.

De quoi est-ce utile? Eh bien, pour beaucoup de choses en fait, mais l'idée est que vous pouvez l'utiliser pour modéliser des choses comme la programmation orientée objet, où les "objets" bundle cachées des données en collaboration avec certaines méthodes de travail sur les données cachées. Ainsi, par exemple, un objet avec les deux méthodes, l'une qui renvoie un Int et un autre qui renvoie un String, pourrait être mise en œuvre de ce type:

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

Comment cela fonctionne? L'objet est mis en œuvre comme une fonction qui a des données internes de type "hidden" a. En fait d'utiliser l'objet, à ses clients de passer dans un "rappel" de la fonction que l'objet d'appels avec les deux méthodes. Par exemple:

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

Nous voici, en gros, en invoquant l'objet de la deuxième méthode, celle dont le type est - a → String pour un inconnu a. Ainsi, à l'insu myObjects clients; mais ces clients ne sais, à partir de la signature, qu'ils seront en mesure d'appliquer l'une des deux fonctions, et d'obtenir soit une Int ou String.

Pour une réelle Haskell exemple, ci-dessous le code que j'ai écrit quand je me suis enseigné RankNTypes. Il implémente un type appelé' ShowBox qui rassemble une valeur d'un type hidden avec ses Show instance de classe. Notez que dans l'exemple en bas, je fais une liste d' ShowBox dont le premier élément est fabriqué à partir d'un nombre, et le second à partir d'une chaîne. Depuis les types sont cachés à l'aide de la plus-rang types, ce n'est pas violer 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 tout le monde la lecture de ce qui s'est demandé comment se fait - ExistentialTypes dans GHC utilise forall, je crois que la raison est parce que c'est à l'aide de ce genre de technique derrière les coulisses.

Answer 2

Ne pas les fonctions en Haskell déjà soutien polymorphes arguments?

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 que les différents types de la même invocation.

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

f g = g 1 + g "lala"

Notez qu'il est parfaitement possible de passer d'une fonction polymorphe comme argument d'une autre fonction. Donc, quelque chose comme map id ["a","b","c"] est parfaitement légal. Mais la fonction ne peut l'utiliser comme monomorphes. Dans l'exemple map utilise id comme si elle avait le type String -> String. Et bien sûr, vous pouvez également passer une simple monomorphe fonction du type donné au lieu de id. Sans rank2types il n'existe aucun moyen pour une fonction d'exiger que son argument doit être une fonction polymorphe et donc aucun moyen de l'utiliser comme une fonction polymorphe.

Answer 3

Luis Casillas réponse donne beaucoup d'info sur ce rang 2 types veux dire, mais je vais simplement vous développez sur un point, il n'a pas de couverture. Nécessitant un argument pour être polymorphe n'est pas seulement lui permettre d'être utilisé avec plusieurs types; elle restreint également que cette fonction peut faire avec son argument(s) et comment il peut produire son résultat. C'est, il donne à l'appelant de moins de flexibilité. Pourquoi voudriez-vous faire cela? Je vais commencer par un exemple simple:

Supposons que nous avons un type de données

data Countries = 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é choisir un des éléments de la liste, elle est donnée, et revenir à un IO action de lancer des missiles sur la cible. Nous pourrions donner des f de type simple:

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

Le problème est que nous pourrions exécutez accidentellement

f (\_ -> BestAlly)

et puis nous serions en grande difficulté! Donner des f grade 1 de type polymorphe

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

n'aide pas du tout, parce que nous choisissons le type d' a lorsque nous appelons f, et de nous spécialiser pour Country et l'utilisation de nos malveillant \_ -> BestAlly de nouveau. La solution est d'utiliser un rang 2 type:

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

Maintenant, la fonction que nous avons pass est requis pour être polymorphe, alors \_ -> BestAlly ne sera pas de vérification de type! En fait, aucune fonction de renvoi d'un élément dans la liste, il est remis typecheck (bien que certaines des fonctions qui vont dans une boucle infinie ou de produire des erreurs et, par conséquent, ne reviennent jamais le fera).

Le ci-dessus est tiré par les cheveux, bien sûr, mais une variante de cette technique est la clé pour faire de l' ST monade coffre-fort.

Answer 4

Voici le lien vers les diapositives du cours Haskell de Bryan O'Sullivan à Stanford qui m'ont aidé à comprendre Rank2Types thingy. http://www.scs.stanford.edu/11au-cs240h/notes/laziness-slides.html