[TYPES] Algorithm W as elaboration into System F

[Ryan Wisnesky]

Hi All,

I’m been trying and unable to find a reference to a full description of Hindley-Milner's type inference algorithm W as a translation of untyped lambda calculus into system F (so that let translates to big lambda etc).  Such a translation is not hard to define - I first encountered it as an exercise in Norman Ramsey’s textbook, but unfortunately that textbook is no longer available, nor did my discussions with Norman turn up a reference.  I’m hoping people here might be able to help.  Somehow, in 2010 it feels like there were a lot more google results on this and many other type theory topics than there are in 2026.

There are of course many papers showing an elaboration into F from a more declarative phrasing of Hindley Milner, because those are easier to work with for many purposes than algorithm W, but I’m looking for a reference for W specifically.  The attached image shows the type part of the untyped to system F translation, so I’m just looking for a reference that shows these rules where let get translated to big lambda and var gets translated to type instantiation etc - the term part of the image.   

Thanks,
Ryan Wisnesky

-------------- next part --------------