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.