[Haskell-cafe] Type Eigenvariable [was: Simple IO Regions]

[oleg at pobox.com]

A good explanation is in Section `1. Eigenvariables and generic reasoning'
of

@inproceedings{MillerTiu,
  author    = {Dale Miller and
               Alwen Fernanto Tiu},
  title     = {A Proof Theory for Generic Judgments: An extended abstract},
  booktitle = {LICS},
  year      = {2003},
  pages     = {118-127},
  url       = \url{http://users.rsise.anu.edu.au/~tiu/lics03sub.pdf},
  crossref  = {DBLP:conf/lics/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/2003,
  title     = {18th IEEE Symposium on Logic in Computer Science (LICS 2003),
               22-25 June 2003, Ottawa, Canada, Proceedings},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year      = {2003},
  isbn      = {0-7695-1884-2},
  key = {LICS},
}

The section explains in which sense eigen-variables are
_variables_. The paper argues, btw, for the separation of those senses
and for a new quantifier to mean uniqueness only. In short, when we
write
	forall x. forall y. body
then x may well be equal to y (in body). And so,
	forall x. forall y. B[x,y] ====> forall z. B[z,z]
OTH, when we write |nabla x. nabla y. body| then x and y are
guaranteed to be different, and so the implication above no longer holds.

Alwen Tiu's web page
	http://users.rsise.anu.edu.au/~tiu/
lists the journal version of the paper.