[Haskell-cafe] forall & ST monad
a.biurvOir4 at asuhan.com
Thu Feb 19 07:22:48 EST 2009
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).
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
 exists! a. (U[a] ->V)
we can constructively derive
 (forall a. U[a]) -> V
even though the program/proof of  derived from  is
deficient as you've explained.
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.
What would be a suitable logic for framing these kinds
of analyses I wonder?
View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22099322.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe