[Haskell-cafe] forall & ST monad

[Kim-Ee Yeoh]

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.