[TYPES] Algorithm W as elaboration into System F

--Apple-Mail=_0FC0DA62-2BFB-49B7-83BD-1AE19B8DF23A
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

--Apple-Mail=_0FC0DA62-2BFB-49B7-83BD-1AE19B8DF23A
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;
	charset=utf-8

Hi All,

I=E2=80=99m 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=E2=80=99s =
textbook, but unfortunately that textbook is no longer available, nor =
did my discussions with Norman turn up a reference.  I=E2=80=99m 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=E2=80=99m looking =
for a reference for W specifically.  The attached image shows the type =
part of the untyped to system F translation, so I=E2=80=99m 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.  =20

Thanks,
Ryan Wisnesky


--Apple-Mail=_0FC0DA62-2BFB-49B7-83BD-1AE19B8DF23A
Content-Transfer-Encoding: 7bit
Content-Type: text/plain;
	charset=us-ascii




--Apple-Mail=_0FC0DA62-2BFB-49B7-83BD-1AE19B8DF23A--