Who invented proxy passing and when?

Question

It seems that until recent years, the usual way to pass an extra type to a function was to do something like

f (undefined :: T) 

Kiselyov and Shan even used this approach in their classic paper on class-based reflection that inspired the reflection package. They excused the obvious ugliness by noting that the bogus value is never inspected. And an only slightly less ugly incarnation appears in Data.Bits.finiteBitSize, which takes a value it ignores to get its type.

Then someone figured out the proxy idiom, and everything changed. Now we always see the much more satisfactory

f (Proxy :: Proxy T) 

(in standard code—GHC type application is another story).

Who figured it out? Did this first appear in code somewhere, or a paper?

Answer 1

A fantastic question. TypeLevelReasoning, an early GHC proposal from April 2013, references the libraries thread "Proxy, new Typeable, and type-level equality" (original poster Richard Eisenberg, the driving force behind many of the recent dependent Haskell work). That thread references another libraries thread "Proxy and new-typeable" (original poster Shachaf Ben-Kiki), which was started in response to a patch from the new-typeable branch. It is difficult to find a record of old branch names and which commits they pointed at, but commit 3d53407 by José Pedro Magalhães seems to be the squashed version of that branch. Indeed it appears to be the first commit landing in GHC to introduce a data Proxy t = Proxy type. Eisenberg would later move that type to Data.Proxy in commit 01aa22b in February 2013. The final design of Proxy seems to be collective synthesis of ideas from many people. However, we can find academic references to Proxy in Magalhães' work, such as his presentation "The right Kind of Generic Programming" (October 2012) and his blog post "Coming soon in GHC HEAD: poly-kinded Typeable" (November 2012). We can probably attribute the inclusion of Proxy in base to him.

However, the idea of a Proxy type seems much older:

• "Giving Haskell a promotion" by Yorgey, Cretin, SPJ (October 2011)

• "Scrap your boilerplate with class" by Lammel, Jones (ICFP 2005)

It is here that my Google searches turn up dry. I cannot seem to find an antecedent to that 2005 paper.

Coda: Shachaf's proposal in that thread, of universally quantifying the proxy type by using forall proxy a. proxy a (which the base libraries still use to this day) instead of forall a. Proxy a is itself interesting, as that and other emails in the thread suggest there at one point might have been multiple instances of Proxy floating around the Haskell ecosystem. As mentioned in the comments, Kmett's tagged library had it back in June 2010.