Qui a inventé le passage par procuration et quand ?

Question

Il semble que jusqu'à ces dernières années, la façon habituelle de passer un type supplémentaire à une fonction était de faire quelque chose comme

f (undefined :: T)

Kiselyov et Shan ont même utilisé cette approche dans leur article classique sur la réflexion en classe qui a inspiré le reflection paquet. Ils ont excusé la laideur évidente en faisant remarquer que la fausse valeur n'est jamais inspectée. Et une incarnation à peine moins laide apparaît dans Data.Bits.finiteBitSize qui prend une valeur qu'il ignore pour obtenir son type.

Puis quelqu'un a découvert l'idiome proxy, et tout a changé. Maintenant, nous voyons toujours la version beaucoup plus satisfaisante

f (Proxy :: Proxy T)

(en code standard - l'application de type GHC est une autre histoire).

Qui a trouvé la solution ? Est-ce que cela est d'abord apparu dans un code quelque part, ou dans un article ?

Answer 1

A fantastique question. TypeNiveauRaisonnement une proposition précoce du GHC datant d'avril 2013, fait référence au libraries filetage "Proxy, nouveau Typeable, et égalité au niveau du type" (l'auteur du message original, Richard Eisenberg, est à l'origine d'une grande partie des travaux récents sur Haskell). Ce fil de discussion fait référence à un autre libraries filetage "Proxy et new-typeable" (poster original Shachaf Ben-Kiki), qui a été lancé en réponse à un correctif de l'application new-typeable branche. Il est difficile de trouver un enregistrement des anciens noms de branches et des commits sur lesquels ils pointaient, mais commit 3d53407 par José Pedro Magalhães semble être la version écrasée de cette branche. En effet, il semble qu'il s'agisse du premier commit atterrissant dans GHC pour introduire une fonction data Proxy t = Proxy type. Eisenberg déplacera plus tard ce type vers Data.Proxy en commettre 01aa22b en février 2013. La conception finale de Proxy semble être une synthèse collective des idées de nombreuses personnes. Cependant, nous pouvons trouver des références académiques à Proxy dans l'œuvre de Magalhães, comme sa présentation "Le bon type de programmation générique" (octobre 2012) et son billet de blog "Bientôt dans GHC HEAD : poly-kinded Typeable" (novembre 2012). Nous pouvons probablement attribuer l'inclusion de Proxy en base à lui.

Cependant, l'idée d'un Proxy Le type semble beaucoup plus vieux :

• "Donner une promotion à Haskell" par Yorgey, Cretin, SPJ (octobre 2011)

• "Débarrassez-vous de vos clichés avec classe" par Lammel, Jones (ICFP 2005)

C'est ici que mes recherches sur Google aboutissent à un résultat sec. Je ne parviens pas à trouver d'antécédent à cet article de 2005.

Coda : la proposition de Shachaf dans ce fil de discussion, de quantifier universellement le type de proxy en utilisant forall proxy a. proxy a (que les bibliothèques de base utilisent toujours à ce jour) au lieu de forall a. Proxy a est en soi intéressant, car ce courriel et d'autres dans le fil de discussion suggèrent qu'il y a eu à un moment donné de multiples instances d'utilisation de l'Internet. Proxy flottant dans l'écosystème Haskell. Comme mentionné dans les commentaires, La bibliothèque étiquetée de Kmett l'avait déjà en juin 2010. .