[TYPES] Algorithm W as elaboration into System F

[Fritz Henglein]

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
>
>
>
>