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