[TYPES] Algorithm W as elaboration into System F

[Ryan Wisnesky]

The missing (presumably filtered) image showed algorithm W, and I’ve tried to write down the original image’s rules as text below.  There’s a similar image available at https://urldefense.com/v3/__https://en.wikipedia.org/wiki/Hindley**BMilner_type_system__;4oCT!!IBzWLUs!Sr5cyWMbhSFuE8_wkQYDFhUb6f4Dlp3hUK15grMs-phBJ_GtufYaUn_nt2-GMDcd05cc_mYpowssatSHsppHhHk6CUUx$  .

(x: forall a. t) in A           
b new
-----------------------  Var rule
A |- x : [a |-> b] t


TA |- E : t
T'TA |- F : t'
T't ~_U t' -> a
a new
------------------------- App rule
UT'TA |- EF : Ua


T(A,x:a) |- E : t
a new
-------------------  Elim rule
TA |- \x.E : Ta -> t


TA |- E : t
o = Gen(TA,t)
T'(TA,x:o) |- F : t'
-----------------------------   Let rule
T'TA |- let x = E in F : t'


To re-state the original question, it’s not hard to enhance these rules to yield a term in system F, where the Var rule term would be a type application and the let rule term a type abstraction, etc but I can’t find a citation for this presumably folklore result.


> On Jul 3, 2026, at 3:21 AM, Jelle Herold <jelle at defekt.nl> wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list  ]
> On Thu, Jun 25, 2026, 8:24 PM Ryan Wisnesky <wisnesky at gmail.com> wrote:
> 
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list  
>> ]
>> Hi All,
>> 
>> [..] The attached image shows [...]
> 
> 
> The image seems to be missing
> 
> Best,
> Jelle