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-mod...