∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitl

∀ 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 http://www.math.ucla.edu/~hbe/amil/index.html