[Haskell-cafe] forall & ST monad

[Dan Doel]

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