Le polymorphisme paramétrique de rang supérieur est-il utile?

Je suis sûr que tout le monde connaît les méthodes génériques du formulaire:

T DoSomething<T>(T item)

Cette fonction est également appelée paramétriquement polymorphe (PP), en particulier PP de rang 1 .

Disons que cette méthode peut être représentée à l'aide d'un objet fonction de la forme:

<T> : T -> T

Autrement dit, <T>cela signifie qu'il prend un paramètre de type, et T -> Tsignifie qu'il prend un paramètre de type Tet renvoie une valeur du même type.

Ensuite, ce serait une fonction PP de rang 2:

(<T> : T -> T) -> int 

La fonction ne prend pas de paramètres de type elle-même, mais prend une fonction qui prend un paramètre de type. Vous pouvez continuer cela de manière itérative, rendant l'imbrication de plus en plus profonde, obtenant un PP de rang de plus en plus élevé.

Cette fonctionnalité est vraiment rare parmi les langages de programmation. Même Haskell ne le permet pas par défaut.

Est-ce utile? Peut-il décrire des comportements difficiles à décrire autrement?

Aussi, qu'est-ce que cela signifie pour quelque chose d' imprédicatif ? (dans ce contexte)

En général, vous utilisez le polymorphisme de rang supérieur lorsque vous voulez que le callee pour pouvoir sélectionner la valeur d'un paramètre de type, plutôt que l' appelant . Par exemple:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

N'importe quelle fonction gque je passe à ceci fdoit pouvoir me donner un à Intpartir d'une valeur d'un certain type, où la seule chose qui gsait à propos de ce type est qu'il a une instance de Show. Ce sont donc casher:

f (length . show)
f (const 42)

Mais ce ne sont pas:

f length
f succ

Une application particulièrement utile consiste à utiliser l'étendue des types pour appliquer l'étendue des valeurs . Supposons que nous ayons un objet de type Action<T>, représentant une action que nous pouvons exécuter pour produire un résultat de type T, tel qu'un futur ou un rappel.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Supposons maintenant que nous avons également un Actionqui peut allouer des Resource<T>objets:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

Nous voulons faire en sorte que ces ressources ne soient utilisées qu'à l'intérieur du lieu Actionoù elles ont été créées, et non partagées entre différentes actions ou différentes exécutions de la même action, afin que les actions soient déterministes et répétables.

Nous pouvons utiliser des types de rang supérieur pour y parvenir en ajoutant un paramètre Saux types Resourceet Action, qui est totalement abstrait - il représente la «portée» du Action. Maintenant, nos signatures sont:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

Maintenant, quand nous donnons runActionun Action<S, T>, nous sommes assurés que parce que le paramètre «scope» Sest entièrement polymorphe, il ne peut pas échapper au corps de runAction- donc aucune valeur d'un type qui utilise Stel que le Resource<S, int>même ne peut s'échapper!

(Dans Haskell, c'est ce qu'on appelle la STmonade, où runActionest appelée runST, Resourceest appelée STRefet newResourceest appelée newSTRef.)

Le polymorphisme de rang supérieur est extrêmement utile. Dans System F (le langage de base des langages FP typés que vous connaissez), cela est essentiel pour admettre les "encodages Church typés", qui est en fait la façon dont System F fait la programmation. Sans cela, le système F est complètement inutile.

Dans le système F, nous définissons les nombres comme

Nat = forall c. (c -> c) -> c -> c

L'addition a le type

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

qui est un type de rang supérieur (le forall c.apparaît à l'intérieur de ces flèches).

Cela se produit également ailleurs. Par exemple, si vous souhaitez indiquer qu'un calcul est un style de passage de continuation approprié (google "codensity haskell"), vous devez corriger cela comme

type CPSed A = forall c. (A -> c) -> c

Même parler d'un type inhabité dans le système F nécessite un polymorphisme de rang supérieur

type Void = forall a. a 

Le long et le court de cela, écrire une fonction dans un système de type pur (système F, CoC) nécessite un polymorphisme de rang supérieur si nous voulons traiter des données intéressantes.

Dans le système F en particulier, ces codages doivent être "imprédicatifs". Cela signifie qu'un forall a.quantifie absolument tous les types . Cela inclut de manière critique le type même que nous définissons. Dans forall a. ace apourrait effectivement se présenter à forall a. anouveau! Dans des langages comme ML, ce n'est pas le cas, on dit qu'ils sont "prédictifs" puisqu'une variable de type quantifie uniquement sur l'ensemble des types sans quantificateurs (appelés monotypes). Notre définition de l' plusimprédicativité requise aussi parce que nous avons instancié l' cin l : Natêtre Nat!

Enfin, je voudrais mentionner une dernière raison pour laquelle vous aimeriez à la fois l'imprédicativité et le polymorphisme de rang supérieur, même dans un langage avec des types arbitrairement récursifs (contrairement au système F). Dans Haskell, il existe une monade d'effets appelée "monade de threads d'état". L'idée est que la monade du thread d'état vous permet de muter les choses mais nécessite d'y échapper pour que votre résultat ne dépende de rien de mutable. Cela signifie que les calculs ST sont remarquablement purs. Pour appliquer cette exigence, nous utilisons un polymorphisme de rang supérieur

runST :: forall a. (forall s. ST s a) -> a

Ici, en veillant à ce qu'il asoit lié en dehors de la portée où nous introduisons s, nous savons que areprésente un type bien formé qui ne dépend pas s. Nous utilisons spour paramétrer toutes les choses mutables dans ce thread d'état particulier afin que nous sachions que cela aest indépendant des choses mutables et donc que rien n'échappe à la portée de ce STcalcul! Un merveilleux exemple d'utilisation de types pour exclure les programmes mal formés.

Soit dit en passant, si vous souhaitez en savoir plus sur la théorie des types, je vous suggère d'investir dans un bon livre ou deux. Il est difficile d'apprendre ces trucs en morceaux. Je suggérerais l'un des livres de Pierce ou Harper sur la théorie du PL en général (et certains éléments de la théorie des types). Le livre "Sujets avancés en types et langages de programmation" couvre également une bonne partie de la théorie des types. Enfin, "Programmation dans la théorie des types de Martin Lof" est une très bonne exposition de la théorie des types intensionnelle que Martin Lof a décrite.