Hi, It goes about the State tansformer monad ST s a. I think how it works but as a logician the use of an internal forall is difficult to swallow. Let's first see a statement in Haskell. One can type foo :: a -> b as a function We can be not sloppy (but this gives unnecessary clutter in the program I think) and type it as: forall a,b foo :: a -> b Now this is a statement in logic, it can be true or false. However what for heaven's sake should I think of 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). Why the use of the inner forall in runST?This is not a normal function declaration in mathematics. Since Haskell is Hindley-Milner typed and can't use an inner forall . Why the use an inner forall. Has imagination dried up (sorry, if this seems impolite)? Thx Scott