Wolfgang Jeltsch-2 wrote: > > Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch: > >> 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. > > Oops, this is probably not true. The statement holds for classical > predicate > logic with only non-empty domains.
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. My apologies for not catching this earlier. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22126043.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe