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