[Haskell-cafe] Re: forall & ST monad
Dan Doel
dan.doel at gmail.com
Tue Feb 17 18:51:21 EST 2009
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)
More information about the Haskell-Cafe
mailing list