[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