On Tue, Feb 17, 2009 at 5:22 AM, Dan Doel
-- 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. I was trying to understand why, so I encoded it into System F: data E p = forall a. E (p a) -- E :: \/p. \/a. p a -> E p -- case_E :: \/p. E p -> \/b. (\/a. p a -> b) -> b data E2 t p = forall a. E2 (t -> p a) -- E2 :: \/t. \/p. \/a. (t -> p a) -> E2 t p -- case_E2 :: \/t. \/p. E2 t p -> \/b. (\/a. (t -> p a) -> b) -> b e11 :: forall t p. (t -> E p) -> E2 t p e11 f = E2 (\t -> case f t of E pa -> pa) -- e11 :: \/t. \/p. (t -> E p) -> E2 t p -- e11 = /\t. /\p. \f :: (t -> E p). -- E2 @t @p @? lose The problem is that the function f may return a different a for each input t, whereas E2 must return the same a for all t. Here's an example: data P a where P :: Num a => a -> P a f :: Bool -> E P f False = E (P (0 :: Int)) f True = E (P (0 :: Integer)) There is no way to encode f in E2; that would specify that the same type a is held in the existential on the rhs of f, but that's not the case here. In particular, if f was held in E2 we would be able to do something like: f_unsound = e11 f unsound = case f_unsound of E2 g -> case g False of P x -> case g True of P y -> x == y According to the signature of e2, x and y are the same type, so there is a type error if e11 typechecks. -- ryan