[TYPES] Algorithm W as elaboration into System F

[Fritz Henglein]

PS: The lecture notes.  Apologies for doubling the number of my emails.

On Sun, Jul 5, 2026 at 1:51 PM Fritz Henglein <fritz at henglein.com> wrote:

> Hi Ryan --
>
> I remember writing the syntax-directed translation of Algorithm W to
> rank-2 bounded System F for a class in 1991.  Alas, I can only find it now
> as an exercise in the introductory lecture notes, made slightly more
> challenging by asking for a translation *after* coding let-expressions as
> lambda-abstractions.  This is essentially the System F rank-2 encoding of
> let-polymorphism.  The lecture notes are included FYI; see Exercise 8.
>
> Best,
> Fritz
>
> PS: I also advised a project Coq-mechanizing of the soundness and
> completeness of Algorithm W wrt. the let-polymorphism type system in that
> class in 1992.  I never tried using Coq myself again after that experience
> -- obviously my bad.
>
> PPS: Warning: Beginning of rambling.  A number of people, myself included,
> have spent quite a bit of effort over the years to get people to not
> actually *literally* implement Algorithm W.  This starts with Milner
> himself in his seminal JCSS 1978 paper, where he describes Algorithm J in
> Section 4.3 as a practical way to implement Algorithm W. ("As it stands, W
> is hardly an efficient algorithm. [...] It was formulated to aid the proof
> of soundness.").   Damas in 1984 formulated let-polymorphism inference by
> simple type inference combined with lazy unfolding of let-definitions,
> which was later shown to work well in practice (monomorphization, papers in
> the mid-90s, MLton, etc).  Hans Leiss and myself (multiple papers, 1987-93)
> showed that let-polymorphism extended to include Mycroft's polymorphic
> recursion, can be compositionally reduced to semi-unification, a constraint
> solving problem with practically fast rewriting on pointer-based data
> structures;  Hans's group built a full version of Standard ML by replacing
> the type inference in SML/NJ (TCS 1999).  Nikolaj Bjørner (ML Workshop
> 1992)  presented Algorithm M (upside-down W) for inferring the locally
> *least* polymorphic types for let-bound variables while maintaining the
> most general type for the whole (global) expression; if you do
> type-directed compilation or analysis you'd rather have g have type int ->
> int in let g x = x in g 5 + g 8 rather than forall 'a. 'a -> 'a.  Still,
> 30+ years later, there seem to be papers and tools where Algorithm W is not
> just, in Robin Milner's words, "formulated to aid the proof of soundness",
> but implemented quite literally. If it works (well enough), it works...
> I'm wondering, though, whether the above rather general and robust (no
> fragile bit-twiddling, cache-performance optimizations or such) techniques
> from the 80s and 90s might be underutilized.  End of rambling.
>
> On Thu, Jun 25, 2026 at 8:21 PM Ryan Wisnesky <wisnesky at gmail.com> wrote:
>
>> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list  ]
>> 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
>>
>>
>>
>>