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

[Francois Pottier]

Hi,

On Mon, Apr 21, 2008 at 03:59:42PM -0600, Jeremy Siek wrote:
> 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.

That's also the way \nu binders float up in the pi-calculus. It is, by now, a
standard way to provide local rewriting rules that explain global generation
of fresh names. Didier and I did not invent anything here. I don't know who
is the earliest inventor of this idea.

Best regards,

-- 
François Pottier
Francois.Pottier at inria.fr
http://cristal.inria.fr/~fpottier/