[Haskell-cafe] Re: forall & ST monad

[Ryan Ingram]

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.  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