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