I got to page 8, where he introduces an upside-down A as I guess a symbol meaning "the set of all" and do not understand even after three readings, anything that is said on page 9.

You guessed pretty much right: ∀ is usually read as for all. It and others he uses (like ⊢ for is derived from) are defined in http://en.wikipedia.org/wiki/List_of_logic_symbols . Hope that helps; as a beginner in Haskell and strong type systems, it looks like I’m going to have trouble with this too.

∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitly in the paper: "The type given for runST above is implicitly universally quantified over both s and a."

We could thus expand the type given for runST as follows: runST is a function which, for every instance of the type a, and every instance of the type s, accepts a state transformer (with type ST s a) and returns a value of type a.

If you want to attain a better understanding of the logical concepts and notation used in the article, try getting hold of an introductory logic text. I recommend Enderton's 'A Mathematical Introduction to Logic'.

http://www.math.ucla.edu/~hbe/amil/index.html

Both your and the previous reply indicate that the blanks I filled in (the "for all" and "derived from" symbols) were indeed as I suspected, and yes I understood the definition of runST to be as you describe it. But I still don't comprehend their discussion of how defining runST thusly somehow provides safety in the example they say it would automatically detect is disallowed.