[Haskell-cafe] Re: forall & ST monad

[Dan Doel]

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