[Haskell-cafe] forall & ST monad
a.biurvOir4 at asuhan.com
Fri Feb 20 14:33:19 EST 2009
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
> 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.
More information about the Haskell-Cafe