Re: [Haskell-cafe] Re: forall & ST monad

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)