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

[Claus Reinke]

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

it has been a very long time, and i don't have the papers at
hand to check my memories, but such things were popular
at a time in the functional logic programming field, with the
subset of fp-background proponents who were fond of
lambda-calculus, explicit scopes, and reduction semantics
(as opposed to the lp-background proponents, who were
more used to dropping their quantifiers). as i said, i'm not
sure about the precise references, but i think the following
two touched on this subject:

@inproceedings{Berkling86b,
  author  = {Klaus Berkling},
  title   = {{Epsilon reduction -- another view of unification}},
  booktitle = {{Fifth Generation Computer Architectures}},
  year    = 1986,
  editor  = {J. V. Wood},
  pages   = {163-176},
  organization = {IFIP},
  publisher = {Elsevier Science Publishers B.V. (North-Holland)},
  topics  = {FP - Lambda Calculi,LP - Unification}
}

@inproceedings{Reddy86b,
  author  = {Uday S.~Reddy},
  title   = {{Functional Logic Languages: Part I}},
  booktitle = {{Graph Reduction, Santa F{\'e}, New Mexico, USA (LNCS 279)}},
  year    = 1986,
  editor  = {J.~H.~Fasel and R.~M.~Keller},
  publisher = {Springer-Verlag},
  topics  = {FP - General,LP - General}
}

dropping choice moves from logic to single-assignment variables,
which suggested the use of similar quantifiers for handling state.

once you let binders "bubble up", you also get another version
of the name capture problem, to which Berkling applied the
same elegant (and underappreciated) solution as he used for
lambda-calculus (see any of the references below).

hth,
claus

@techreport{Berkling76,
  author  = {Berkling, K.J.},
  title   = {{A Symmetric Complement to the Lambda Calculus}},
  institution = GMD,
  note    = {ISF-76-7},
  month   = {September},
  year    = 1976,
  abstract =  {"The calculi of Lambda-conversion" introduced by A.Church
  are complemented by a new operator lambda-bar, which is in
  some sense the inverse to the lambda-operator. The main
  advantage of the complemented system is that variables do
  not have to be renamed. Conversely, any renaming of
  variables in a formula is possible. Variables may, however,
  appear with varied numbers of lambda-bars in front of them.
  Implementations of the lambda calculus representation with
  the symmetric complement are greatly facilitated.

  In particular, a renaming of all variables in a formula to
  the same one is possible. Variables are then distinguished
  only by the number of preceding lambda-bars. Finally, we
  give a four symbol representation of the lambda calculus
  based on the above mentioned freedom in renaming.  },
  topics  = {FP - Lambda Calculi}
}

@article{BerklingFehr82a,
  author  = {Klaus Berkling and E. Fehr},
  title   = {{A Consistent Extension of the Lambda Calculus as a Base for Functional Programming 
Languages}},
  journal = {Information and Control},
  volume  = {55},
  number  = {1-3},
  pages   = {89-101},
  year    = 1982,
  topics  = {FP - Lambda Calculi}
}

@article{BerklingFehr82b,
  author  = {Klaus Berkling and E. Fehr},
  title   = {{A modification of the $\lambda$-calculus as a base for functional programming 
languages}},
  journal = {{Lecture Notes in Computer Science}},
  volume  = {140},
  pages   = {35-47},
  year    = 1982,
  topics  = {FP - Lambda Calculi}
}