[TYPES] analogy between Felleisen's syntactic theories of state and Hindley-Milner constraints

[Jeremy Siek]

Dear Types Readers,

I was recently reading Felleisen and Hieb's "The revised report on  
syntactic
theories of sequential control and state" and also Francois Pottier
and Didier Remy's "The Essence of  ML Type Inference" and
was struck by the similarity between the \rho binder in the \Lambda_ 
\sigma
calculus and and the \exists binder in the language of constraints. They
both provide a local way to generate fresh variables. Also, the  
semantics
of how these binders "bubble up" through the program is quite similar.
I'm curious if they have a shared ancestry or whether there were two
independent branches of discovery. It seems like this technique deserves
the status of a "design pattern" for dealing with the generation of  
fresh variables.
I'm also curious about other applications of this technique.

Cheers,
Jeremy