[Haskell-cafe] forall & ST monad
Dan Doel
dan.doel at gmail.com
Thu Feb 19 08:09:44 EST 2009
On Thursday 19 February 2009 7:22:48 am Kim-Ee Yeoh wrote:
> Jonathan Cast-2 wrote:
> > 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).
>
> Interesting.
>
> What's going on in the example that you posted seems to be a
> stronger but still familiar version of "there exists", namely "there
> exists exactly one" a.k.a. "there uniquely exists", often represented
> with exists-bang: "exists!".
>
> The problem is that given
>
> [1] exists! a. (U[a] ->V)
>
> we can constructively derive
>
> [2] (forall a. U[a]) -> V
>
> even though the program/proof of [2] derived from [1] is
> deficient as you've explained.
I don't think there's anything wrong with that. The forall version works for
ST refs, and the exists version does not. This is generalized by the fact that
one cannot write a function with type:
((forall a. U[a]) -> V) -> (exists a. U[a] -> V)
By contrast, the fact that you can write a function with type:
(exists a. U[a] -> V) -> ((forall a. U[a]) -> V)
would indicate that anything that can be handled with the exists type could
also be handled by the forall type.
> In Haskell, the only existential quantification is exists-bang.
> The weaker form of existence is sufficient to regain thread safety
> for runST. Every application of a program of type
> (exists-w/o-bang a. U[a]) simply cannot assume that the (a) is
> always the same.
Correct me if I'm wrong, but isn't this 'merely' what the constructive
existential is (which is what you get in the usual type theories, not the
classical existential)? An existential:
exists a:T. P(a)
is a pair of some a with type T and a proof that a satisfies P (which has type
P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. That
doesn't mean that there is only one a:T for which P is satisfied. But it
*does* mean that for any particular proof of exists a:T. P(a), only one a:T is
involved. So if you can open that proof, then you know that that is the
particular a you're dealing with, which leads to the problems in the
grandparent.
Cheers,
-- Dan
More information about the Haskell-Cafe
mailing list