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