Question aboutthe use of an inner forall

Jon Cast
Mon, 19 Aug 2002 13:46:24 -0500

"Scott J." <> wrote:
> Well I don't feel alone anymore.

> Here follows how I think runST :: (forall s. ST s a) -> a works:

> if a is represented by e.g. MutVar s a . Then the compiler complains
> because it did find an s in the "data" represented by a. This s must
> first be eliminated by some other combinators(?).

Right.  The `s' is appearing outside the area it is defined in.

> I agree that something must be written for the argument of runST to
> warn programmers about the possible "representations" of a. But I
> still have problems that one has chosen forall.

`forall' and `Pi' are the basic names for this sort of thing in type
theory.  See the discussion of the Howard-Curry isomorphism for
`forall'.  You probably don't want to know about `Pi'.

> Scott

Jon Cast