Jonathan Cast jonathanccast at fastmail.fm
Mon Feb 16 16:44:39 EST 2009

```On Mon, 2009-02-16 at 19:36 +0100, Wolfgang Jeltsch wrote:
> Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
> > Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:
> > > Despite its rank-2 type, runST really doesn't have anything to do with
> > > existential quantification.
> >
> > First, I thought so too but I changed my mind. To my knowledge a type
> > (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T').
> > It’s the same as in predicate logic – Curry-Howard in action.
>
> Oops, this is probably not true. The statement holds for classical predicate
> logic with only non-empty domains. But in constructivist logic only the first
> of the above statements follows from the second, not the other way round.

Not only that, but giving runST an existential type would defeat its
safety properties.  Taking the `let open' syntax from `First-class
Modules for Haskell' [1], we can say

let open runST' = runST in
let
ref = runST' \$ newSTRef 0
!() = runST' \$ writeSTRef ref 1
!() = runST' \$ writeSTRef ref 2

This type-checks because the let open gives us the *same* skolemized
constant for s everywhere in the sequel.  Now, the above de-sugars to

let open runST' = runST in
let
ref = runST' \$ newSTRef 0
x   = runST' \$ writeSTRef ref 1
y   = runST' \$ writeSTRef ref 2
in case x of () -> case y of () -> runST' \$ readSTRef ref

Haskell's semantics (if we could write runST in Haskell) would let us
re-order the cases in this instance --- with changes the over-all value
from 2 to 1.  In fact, if you inline x and y, you can discard the cases
entirely, so the expression has value 0.

Summary: Existential types are not enough for ST.  You need the rank 2
type, to guarantee that *each* application of runST may (potentially)
work with a different class of references.  (A different state thread).

jcc

[1] http://research.microsoft.com/en-us/um/people/simonpj/papers/first-class-modules/index.htm

```