[Haskell-cafe] Re: forall & ST monad

[Dan Doel]

On Tuesday 17 February 2009 5:27:45 pm Ryan Ingram wrote:
> On Tue, Feb 17, 2009 at 5:22 AM, Dan Doel <dan.doel at gmail.com> 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)