Fw: Question about the use of an inner forall

[oleg@pobox.com]

> Leon Smith wrote:

> >On Friday 16 August 2002 23:57, Scott J. wrote:
> >runST :: forall a ( forall s ST s a) -> a ?
> >
> >In logic forall x forall y statement(x.y) is equivalent to:
> >  forall y forall x statement(x,y). 
> Now, using a different argument, since "s" does not appear free on
> the R.H.S of the implication, "forall s" can be moved outside the
> implication to quantify over the entire type.

I'm afraid I disagree -- in general, we can't move quantifiers in and
out with impunity.

In our example:

	all a. ( (all s. ST s a) => a )
===
	all a. ( !(all s. ST s a) | a )
===
	all a. ( (exists s. !(ST s a)) | a )
=== {using identity (exists x. p) | q === exists x. (p|q) where x is
not free in q}
===     all a. (exists s. (!(ST s a) | a))
===	all a. exists s. (ST s a => a)

So, the type of runST is runST::exists s. (ST s a -> a)
Alas, we can't use 'exists' quantifier in type expressions; therefore,
we have to use the round-about trick with forall, on the _left-hand_
side of the implication.

> Jon Cast wrote:
> Polymorphic types form a sub-typing system, with the basic
> sub-typing judgment:
 
> (forall a. S) < [T/a]S 


I'd like to note a parallel with lambda-Prolog: If S is the set of
type declarations and P is the set of program clauses, to prove
(forall x::T. G) from <S,P>, we introduce a new unique _constant_ c of
type T and attempt to prove [c/x]G from <S U {c},P>

OTH, to prove (exists x::T . G) from <S,P>, we prove [_X/x]G from
<S,P> where _X is just a (unbound) Prolog variable. We let the
standard unification mechanism to bind _X to something that makes G
true.

On the subject of escaping of quantified variables, the lambda-Prolog
Tutorial by Amy Felten gives an interesting example:

	?- append (1::2::nil) z X.
the answer is X == (1::2::z).

	?- pi y\( append (1::2::nil) y X).
the answer is NO. Indeed, as outlined before, we first choose a
unique constant k and attempt to prove
	?- append (1::2::nil) k X.
The proof seemingly succeeds, with X bound to (1::2::k). However,
this binding causes 'k' to 'escape'. Therefore, this binding is
rejected, and the proof falls apart. Which indeed makes sense: the
value of X that makes pi y\( append (1::2::nil) y X) true should not
depend on any particular value of y. Only in this case the expression
would be true for all y.

	?- pi y\( append (1::2::nil) y (H y)).
actually succeeds, with H bound to w\(1::2::w).