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

[Bill Wood]

On Thu, 2006-01-19 at 19:18 -0800, oleg at pobox.com wrote:
   . . . 
> _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.

OK, I gotta ask: is |nabla x, nabla y. phi(x,y)| logically equivalent to
|forall x, forall y. x <> y only-if phi(x,y)|?  I use |P only-if Q| for
|P materially implies Q|.

 -- Bill Wood