[Haskell-cafe] forall & ST monad

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
  in runST' $ readSTRef ref

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



More information about the Haskell-Cafe mailing list