2009/2/15 Brandon S. Allbery KF8NH

On 2009 Feb 15, at 11:50, Peter Verswyvelen wrote:

I could try to read the article a couple of times again, but are there any other good readings about these existentially quantified types and how the ST monad works?

You could think about it as playing a dirty trick on the typechecker.

But if you don't want to, there's another way to think about it. I'm still working on this interpretation, so be gentle :-) Think of the s in ST s a not as a type, but as itself a "state"; eg. a map from keys to values and a free list of fresh keys. This is the initial state of the computation, which ST transforms. Then runST says: runST :: (forall s. ST s a) -> a If a computation works on every initial state, we can extract the value. Since it works for every initial state, it must not depend on it, and thus the computation's value is well-defined. Something like that. I think using existential types as regions is more essential than a "dirty trick", and I advocate trying to interpret it in a semantically well-defined way. Luke

On Sun, Feb 15, 2009 at 11:50 AM, Kim-Ee Yeoh wrote:

Having said that, I'm not sure about the statement on page 9 that "readVar v simply does not have type forall s. ST s Bool." The variable v could be of type "forall s. MutVar s Bool", in which case all of "runST (readVar v)" typechecks.

"readVar v" can't have the type (forall s. ST s Bool), because v must have been created by newVar. So, (newVar True >>= \v -> readVar v) has the type (forall s. ST s Bool), but the subexpression (readVar v) has the type ST hiddenState Bool, where hiddenState is constrained to match the same state as was used by newVar and bind (>>=). Decoding into System F might make this more explicit: newVar :: forall t s. t -> ST s (MutVar s t) readVar :: forall t s. MutVar s t -> ST s t bind :: forall a b s. ST s a -> (a -> ST s b) -> ST s b Then the expression is: /\s -> bind @(MutVar s Bool) @Bool @s (newVar @Bool @s True) (\(v :: MutVar s Bool) -> readVar @Bool @s v) (where /\ is a type-level lambda, and @ is used for type-level application, that is, to remove one layer of "forall" from a type.) Note that there is no way to turn the insides of that final lambda expression into something that uses any "s" without getting something of type "forall s. MutVar s Bool". But there's no way to do so because newVar only returns results of type "forall s. ST s (MutVar s Bool)"; then s is constrained to match during the binding application. Then, looking at the type of runST: forall t. (forall s. ST s t) -> t, you see that runST must be passed an argument that has a type level lambda for s, saying that runST gets to choose the type "s" used to call it. In particular, in GHC I believe that s is always instantiated with RealWorld# when runST uses its argument, but you never get to see that. runST is just unsafePerformIO made safe by making the Real World "hidden" in the forall so that it can't escape. -- ryan

Aha! Wolfgang is a man who knows his own code :) Yes, I've seen this a couple of times but when I saw it again in Grapefruit, I wanted to know how this usage of existentials worked, since I'm sooo curious to find out how you managed to use the type system for solving some of the typical FRP problems. I have plenty of references now to study, so hopefully I will get one step further with Grapefruit. Thanks! On Mon, Feb 16, 2009 at 1:30 PM, Wolfgang Jeltsch < g9ks157k@acme.softbase.org> wrote:

Am Sonntag, 15. Februar 2009 17:50 schrieb Peter Verswyvelen:

...

I'm having trouble understanding the explanation of the meaning of the signature of runST

Were you just reading the documentation of Grapefruit's era parameters or why are you studying ST? ;-)

Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:

Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:

...

Despite its rank-2 type, runST really doesn't have anything to do with existential quantification.

First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.

Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains. But in constructivist logic only the first of the above statements follows from the second, not the other way round. So arguing with the Curry-Howard isomorphism fails and indeed, the two types are not equivalent. There is just a function from the second to the first (it’s the function application function ($) actually). Best wishes, Wolfgang

On Mon, 2009-02-16 at 19:36 +0100, Wolfgang Jeltsch wrote:

Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:

...

Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:

...

Despite its rank-2 type, runST really doesn't have anything to do with existential quantification.

First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.

Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains. But in constructivist logic only the first of the above statements follows from the second, not the other way round.

Not only that, but giving runST an existential type would defeat its safety properties. Taking the `let open' syntax from `First-class Modules for Haskell' [1], we can say let open runST' = runST in let ref = runST' $ newSTRef 0 !() = runST' $ writeSTRef ref 1 !() = runST' $ writeSTRef ref 2 in runST' $ readSTRef ref This type-checks because the let open gives us the *same* skolemized constant for s everywhere in the sequel. Now, the above de-sugars to let open runST' = runST in let ref = runST' $ newSTRef 0 x = runST' $ writeSTRef ref 1 y = runST' $ writeSTRef ref 2 in case x of () -> case y of () -> runST' $ readSTRef ref Haskell's semantics (if we could write runST in Haskell) would let us re-order the cases in this instance --- with changes the over-all value from 2 to 1. In fact, if you inline x and y, you can discard the cases entirely, so the expression has value 0. 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). jcc [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/first-class-mod...

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

On Thu, 2009-02-19 at 05:53 -0800, Kim-Ee Yeoh wrote:

There's a lot to chew on (thank you!), but I'll just take something I can handle for now.

Dan Doel wrote:

...

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.

re: Constructivity and the opening of a proof

A form of the theorem that the primes are infinite goes "Given a finite set of primes, there's a prime bigger than any of them."

The usual proof is constructive since factorization is algorithmic, but I don't see why a priori, applications of this theorem on a given input should always yield the same prime when more than one factor exists.

They don't. Any particular constructive proof will yield a particular new bigger prime, but they don't have to yield the same one. Let's choose a simpler example: There exists an Integer. Any (constructive) proof of that proposition is just an Integer and thus certainly a particular Integer. However, there is nothing special about any particular Integer.

Is non-deterministic choice forbidden in constructive math? A cursory google seems to suggest that if not, it's at least a bête noire to some.

Not particularly, but if you ultimately want an executable algorithm, you are sooner or later going to have to spell out how such a non-deterministic choice is made. -Proof-search-, though, is usually quite non-deterministic.

Wolfgang Jeltsch-2 wrote:

Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:

...

First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.

Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains.

Here's a counterexample, regardless of whether you're using constructive or classical logic, that (forall a. T[a]) -> T' does not imply exists a. (T[a] -> T'). Let a not exist, but T' true. Done. My apologies for not catching this earlier. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22126043.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

Ryan Ingram wrote:

It believe that it's true that ((forall a. t a) -> t') does not entail (exists a. t a -> t') in constructivist logic, but I can't come up with a proof off the top of my head. Intuitively, to construct a value of type (E t t') you need to fix an "a", and I don't think it's possible to do so.

Here's something close to a counterexample, but I'm really confused. The objects of discourse are red, blue and green glass marbles T[a] = a is red \/ a is blue S = forall a. T[a] = all marbles are red or blue Now, (forall a. T[a]) -> S is clearly true while exists a. (T[a] -> S) should be nonsense: having one example of a marble that is either red or blue does in no way imply that all of them are, at least constructively. (It is true classically, but I forgot the name of the corresponding theorem.) I'm not quite sure how to make that rigorous; I would like to turn the above into a proper model of intuitionistic logic. The other problem is that in Haskell, forall does not quantify over glass marbles, but over types/propositions. Take T[a] = a S = forall a. T[a] = _|_ Once again, (forall a. T[a]) -> S is true, but what about exists a. (a -> _|_) = exists a. not a ? I mean, a can be a proposition now, so what about taking a = forall b.b = _|_ ? Does exists a imply that the example proposition constructed should true or is it enough to be able to construct a proposition at all? Regards, apfelmus -- http://apfelmus.nfshost.com

On Wed, 2009-02-25 at 10:18 -0800, Kim-Ee Yeoh wrote:

Heinrich Apfelmus wrote:

...

Now,

(forall a. T[a]) -> S

is clearly true while

exists a. (T[a] -> S)

should be nonsense: having one example of a marble that is either red or blue does in no way imply that all of them are, at least constructively. (It is true classically, but I forgot the name of the corresponding theorem.)

For the record, allow me to redress my earlier erroneous assertion by furnishing the proof for the classical case:

(forall a. T(a)) -> S = not (forall a. T(a)) or S, by defn of implication

[For the record: this is the first point at which you confine yourself to classical logic.]

= not $ (forall a. T(a)) and (not S), by de Morgan's = not $ forall a. T(a) and (not S), product rule???

This step depends on the domain of quantification for the variable a being non-empty; if the domain is empty, then the RHS is vacuously true, while the LHS is equal to (not S).

= exists a. not (T(a)) or S, de Morgan's again = exists a. T(a) -> S, by defn of implication

The only wrinkle is obviously in the logical "and" of (not S) distributing under the universal quantifier.

jcc

On Tuesday 17 February 2009 7:28:18 am Heinrich Apfelmus wrote:

Wolfgang Jeltsch wrote:

...

First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.

The connection is the other way round, I think.

(exists a. T[a]) -> T' = forall a. (T[a] -> T')

You are correct. Your equation works both ways, while the other only works in one direction. Some experiments: {-# LANGUAGE ExistentialQuantification, RankNTypes #-} module E where data E p = forall a. E (p a) data E' p t = forall a. E' (p a -> t) data E'' t p = forall a. E'' (t -> p a) -- fail: a doesn't match a1 -- (exists a. p a -> t) -> (exists a. p a) -> t -- e1 :: E' p t -> (E p -> t) -- e1 (E' f) (E pa) = f pa -- works -- ((exists a. p a) -> t) -> (exists a. p a -> t) e2 :: (E p -> t) -> E' p t e2 f = E' (\pa -> f (E pa)) -- works -- ((exists a. p a) -> t) <-> (forall a. p a -> t) e3 :: (E p -> t) -> (forall a. p a -> t) e3 f = \pa -> f (E pa) e4 :: (forall a. p a -> t) -> (E p -> t) e4 f (E pa) = f pa -- fail: inferred type less polymorphic than expected -- ((forall a. p a) -> t) -> (exists a. p a -> t) -- e5 :: ((forall a. p a) -> t) -> E' p t -- e5 f = E' (\pa -> f pa) -- works -- (exists a. p a -> t) -> ((forall a. p a) -> t) e6 :: E' p t -> (forall a. p a) -> t e6 (E' f) pa = f pa -- fail: a doesn't match a1 -- ((forall a. p a) -> t) -> ((exists a. p a) -> t) -- e7 :: ((forall a. p a) -> t) -> (E p -> t) -- e7 f (E pa) = f pa -- works, of course -- ((exists a. p a) -> t) -> ((forall a. p a) -> t) e8 :: (E p -> t) -> ((forall a. p a) -> t) e8 f pa = f (E pa) -- e8 f = e6 (e2 f) -- e8 f = e9 (e3 f) -- works e9 :: (forall a. p a -> t) -> ((forall a. p a) -> t) e9 f pa = f pa -- fail: a1 does not match a -- e10 :: ((forall a. p a) -> t) -> (forall a. p a -> t) -- e10 f pa = f pa -- fail: inferred type less polymorphic than expected -- This seems like it could perhaps work, since E'' -- re-hides the 'a' but it doesn't, probably because there's -- no way to type the enclosed lambda expression properly. -- You'd probably need support for something like what Jonathan -- Cast used in his mail. -- (t -> (exists a. p a)) -> (exists a. t -> p a) -- e11 :: (t -> E p) -> E'' t p -- e11 f = E'' (\t -> case f t of E pa -> pa) -- works -- (exists a. t -> p a) -> (t -> (exists a. p a)) e12 :: E'' t p -> (t -> E p) e12 (E'' f) t = E (f t) -- works e13 :: (forall a. t -> p a) -> (t -> (forall a. p a)) e13 f t = f t -- works e14 :: (t -> (forall a. p a)) -> (forall a. t -> p a) e14 f t = f t

On Tuesday 17 February 2009 5:27:45 pm Ryan Ingram wrote:

On Tue, Feb 17, 2009 at 5:22 AM, Dan Doel wrote:

...

-- fail: inferred type less polymorphic than expected -- This seems like it could perhaps work, since E'' -- re-hides the 'a' but it doesn't, probably because there's -- no way to type the enclosed lambda expression properly. -- You'd probably need support for something like what Jonathan -- Cast used in his mail. -- (t -> (exists a. p a)) -> (exists a. t -> p a) -- e11 :: (t -> E p) -> E'' t p -- e11 f = E'' (\t -> case f t of E pa -> pa)

This can't work.

Ah! Good catch. I was sort of motivated by the rule: (forall a. t -> p a) <==> t -> (forall a. p a) I figured that there'd be a similar rule for exists, but both: (exists a. p a -> t) ==> (exists a. p a) -> t and: (t -> exists a. p a) ==> (exists a. t -> p a) were failing. The latter seemed like the more likely case to be possible, since just eyeballing it, it looked like it could be an implementation artifact (lack of first-class existentials). As consolation, here are some additional rules, which one can look up on wikipedia's article on intuitionistic logic to see that they match: ---- snip ---- needs EmptyDataDecls ---- data Void -- works -- (exists a. p a) -> (not (forall a. not (p a))) -- e15 :: E p -> (forall r. (forall a. p a -> r) -> r) e15 :: E p -> (forall a. p a -> Void) -> Void e15 (E pa) k = k pa -- (not (forall a. not (p a))) -> exists a. p a -- e16 :: (forall r. (forall a. p a -> r) -> r) -> E p -- works here -- e16 :: ((forall a. p a -> Void) -> Void) -> E p -- fails here E p /= Void -- e16 f = f E -- works -- (forall a. p a) -> (not (exists a. not (p a))) -- e17 :: (forall a. p a) -> (forall r. E' p r -> r) e17 :: (forall a. p a) -> (E' p Void -> Void) e17 pa (E' f) = f pa -- (not (exists a. not (p a))) -> (forall a. p a) -- e18 :: (forall r. E' p r -> r) -> (forall a. p a) -- works -- e18 :: (E' p Void -> Void) -> (forall a. p a) -- fail: Void /= p a -- e18 f = f (E' id) -- be careful about how you encode your negation. :) -- using (forall r. r) in place of Void also works, giving slightly more -- cryptic error messages. -- works -- (exists a. not (p a)) -> not (forall a. p a) e19 :: (E' p Void) -> (forall a. p a) -> Void e19 (E' f) pa = f pa -- works -- (forall a. not (p a)) -> not (exists a. p a) e20 :: (forall a. p a -> Void) -> E p -> Void e20 f (E pa) = f pa -- works -- (not (exists a. p a)) -> (forall a. not (p a)) e21 :: (E p -> Void) -> (forall a. p a -> Void) e21 f pa = f (E pa)