PureScript "inner" quantified type

Question

I assume I got the terminology in the tile wrong - let me know what I should have used instead for the below.

In PureScript by Example, section 8.17 Mutable State, there's a discussion of the type of runST:

runST :: forall a eff. (forall h. Eff (st :: ST h | eff) a) -> Eff eff a

The thing to notice here is that the region type h is quantified inside the parentheses on the left of the function arrow. That means that whatever action we pass to runST has to work with any region h whatsoever.

I understand the end goal, but can someone clarify this statement from the perspective of types and how this gets restricted as per above?

If possible, can the difference be shown on simpler types, e.g. what is the difference between:

f1 :: forall i o. Array i -> Array o
f2 :: forall o. (forall i. Array i) -> Array o

I think a short example would help.

Answer 1

What values inhabit the type Array a?

Well, if you know what a is, or something about a, then you might be able to give concrete examples. If a is known to be Int, then [1, 2, 3] is a fine answer. If a has a Monoid instance then [mempty] works. However, if you don't know anything about a then the only answer you can confidently give is [].

What values inhabit the type forall a. Array a?

Any value inhabiting that type has to inhabit Array a for any choice of a. Since we don't know anything about a, the answer is "only []" again. So the forall constrains us to only a single possible implementation of a type in this case.

Now forall a. Array a is a type like any other, so it can appear as the argument type of a function. As a caller of such a function, you only have one possible value that you can provide. As the implementor of that function, you can choose to use the argument with any type a (since it must work with whatever type you choose).

The same is true for runST. The implementor of runST can choose to call your action with any h it pleases, so it (conceptually) generates a new memory region for you to work with. As the caller, you have to work with whatever memory region you are given, without knowing anything about it. This means that you can only use the actions provided (newSTRef, writeSTRef, etc.) abstractly, and any references you create cannot leave the scope of the runST block (the type variable h doesn't exist outside that scope, after all), which allows runST to return a pure result safely.

So, forall is a useful tool for restricting the values that can be provided as function arguments.