[Haskell-cafe] Type Eigenvariable [was: Simple IO Regions]
Bill Wood
william.wood3 at comcast.net
Fri Jan 20 00:48:12 EST 2006
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
More information about the Haskell-Cafe
mailing list