[Haskell-cafe] forall & ST monad

[Ryan Ingram]

On Fri, Feb 20, 2009 at 11:33 AM, Kim-Ee Yeoh <a.biurvOir4 at asuhan.com> wrote:
> Here's a counterexample, regardless of whether you're using
> constructive or classical logic, that (forall a. T[a]) -> T' does
> not imply exists a. (T[a] -> T').
>
> Let a not exist, but T' true. Done.

That isn't quite a proper counterexample; if T' is true, that is, you
can write a term of type T', then exists a. (T[a] -> T') is trivially
true; here's a constructivist proof in Haskell:

type T :: * -> * -- given
type T' :: * -- given

v :: T'
v = given

type A = ()
f :: T A -> T'
f _ = v

data E t t' where E :: forall t t' a. (t a -> t') -> E t t'
proof :: E T T'
proof = E f

It believe that it's true that ((forall a. t a) -> t') does not entail
(exists a. t a -> t') in constructivist logic, but I can't come up
with a proof off the top of my head.  Intuitively, to construct a
value of type (E t t') you need to fix an "a", and I don't think it's
possible to do so.

On the other hand, "a" is hidden, so the only way to call the function
inside of E t t' is to pass it something of type (forall a. t a),
right?

  -- ryan